While the benefits of the ExCAPE approach will apply broadly to software development, to understand the viability and roadblocks for the proposed approach, the ExCAPE team focuses its efforts by initially targeting five challenge problems. These problems are representative of the complexity of modern cyber-physical systems on networked multi-core platforms. These include:
Imagine a robot waiter having to surve customers with plates. Can we formalize its specification and automatically synthesize his behavior? How can he cope with the different data on the menu? If another waiter robot broke a glass, can he avoid trumpling over it on his way to the kitchen? How can we design it in a composite way, leveraging working provable subcomponents?
Design of robotic systems, being complete autonomous machines, involves many facets that are absent in the design of other computerized systems. The robotics theme thus present new challenges for automatic synthesis as envisioned by ExCAPE. Motion planning is a prominent example. ExCAPE researchers have developed an open source motion planning library implementing motions solvers that allow the satisfaction of a high level specification while at the same time ensuring a feasible robot motion plan is produced. Other researched areas include synthesis in partially unknown environments, syntheis with costs, synthesis with complex dynamics, and synthesis for multi-robot motion planning.
Traditional internet routing systems involve precise configuration of many low-level parameters on each network devise. Software-defined networks (SDN) is an emerging approach to computer networking which abstracts away these lower level details from the traffic specification, thus allowing network routing reasoning at a higher abstraction level. ExCAPE researchers are exploring synthesis in both traditional internet routing systems, as well as in the software-defined networks emerging approach.
Smart-phones and tablets have recently entered our lives and have gained popularity in an unprecedented rapidness. So has the variety and amount of application that run on mobile devices. Programming for mobile devices encounters some obstacles that are absent in programming for traditional computers. For instance, mobile operating systems such as Andorid and iOS are updated in a frequent manner, requiring the program and its analysis be robust to such changes. Another example has to do with visualization, as applications run both on very small screens and on a variety of different sizes screen, each phenomenon incurring its own set of difficulties. These, and other obstacles unique to mobile apps, offer an opportunity to leverage ExCAPE synthesis solutions to improve productivity of programmers on mobile platforms.
Hardware communication and coordination protocols are the backbone of today’s highly integrated Systems-on-Chip (SoC) designs, which are ubiquitous in mobile and embedded computing platforms. Even when employing the stateof- the-art design practices, designers are still called upon to create the entire design, including the most mundane but error-prone low-level aspects of the design, which arguably leads to tedious design and presence of bugs. The goal of this theme is to explore how synthesis can simplify and improve the design process for multicore protocols.
With the increasing importance of online education, we have realized that technology for formal verification and synthesis can contribute to online learning by analyzing students’ solutions to provide meaningful, personalized explanation of their mistakes, and also by automatic grading. We have built such tools for representative topics in three undergraduate courses: introduction to programming, theory of computation, and design of cyber-physical systems. The design of these tools not only uses computational engines built for synthesis by ExCAPE researchers, but also integrates HCI research on user interaction and tool evaluation.
Click one of the above items for more info or visit the publications page for papers under the challenge problems theme.