TY - CONF AB - The assume-guarantee paradigm is a powerful divide-and-conquer mechanism for decomposing a verification task about a system into subtasks about the individual components of the system. The key to assume-guarantee reasoning is to consider each component not in isolation, but in conjunction with assumptions about the context of the component. Assume-guarantee principles are known for purely concurrent contexts, which constrain the input data of a component, as well as for purely sequential contexts, which constrain the entry configurations of a component. We present a model for hierarchical system design which permits the arbitrary nesting of parallel as well as serial composition, and which supports an assume-guarantee principle for mixed parallel-serial contexts. Our model also supports both discrete and continuous processes, and is therefore well-suited for the modeling and analysis of embedded software systems which interact with real-world environments. Using an example of two cooperating robots, we show refinement between a high-level model which specifies continuous timing constraints and an implementation which relies on discrete sampling. AU - Henzinger, Thomas A AU - Minea, Marius AU - Prabhu, Vinayak ID - 4477 SN - 9783540418665 T2 - Proceedings of the 4th International Workshop on Hybrid Systems TI - Assume-guarantee reasoning for hierarchical hybrid systems VL - 2034 ER - TY - CONF AB - Giotto is a principled, tool-supported design methodology for implementing embedded control systems on platforms of possibly distributed sensors, actuators, CPUs, and networks. Giotto is based on the principle that time-triggered task invocations plus time-triggered mode switches can form the abstract essence of programming real-time control systems. Giotto consists of a programming language with a formal semantics, and a retargetable compiler and runtime library. Giotto supports the automation of control system design by strictly separating platform-independent functionality and timing concerns from platform-dependent scheduling and communication issues. The time-triggered predictability of Giotto makes it particularly suitable for safety-critical applications with hard real-time constraints. We illustrate the platform-independence and time-triggered execution of Giotto by coordinating a heterogeneous flock of Intel x86 robots and Lego Mindstorms robots. AU - Henzinger, Thomas A AU - Horowitz, Benjamin AU - Kirsch, Christoph ID - 4478 SN - 9781581134254 T2 - Proceedings of the 2nd ACM SIGPLAN workshop on Languages, compilers and tools for embedded systems TI - Embedded control systems development with Giotto ER - TY - CONF AB - Giotto provides an abstract programmer’s model for the implementation of embedded control systems with hard real-time constraints. A typical control application consists of periodic software tasks together with a mode switching logic for enabling and disabling tasks. Giotto specifies time-triggered sensor readings, task invocations, and mode switches independent of any implementation platform. Giotto can be annotated with platform constraints such as task-to-host mappings, and task and communication schedules. The annotations are directives for the Giotto compiler, but they do not alter the functionality and timing of a Giotto program. By separating the platform-independent from the platform-dependent concerns, Giotto enables a great deal of flexibility in choosing control platforms as well as a great deal of automation in the validation and synthesis of control software. The time-triggered nature of Giotto achieves timing predictability, which makes Giotto particularly suitable for safety-critical applications. AU - Henzinger, Thomas A AU - Horowitz, Benjamin AU - Kirsch, Christoph ID - 4479 SN - 9783540426738 T2 - Proceedings of the 1st International Workshop on Embedded Software TI - Giotto: A time-triggered language for embedded programming VL - 2211 ER - TY - CONF AB - We provide an overview of the current status of HYTECH, and reflect on some of the lessons learned from our experiences with the tool. HYTECH is a symbolic model checker for mixed discrete-continuous systems that are modeled as automata with piecewise-constant polyhedral differential inclusions. The use of a formal input language and automated procedures for state-space traversal lay the foundation for formally verifying properties of hybrid dynamical systems. We describe some recent experiences analyzing three hybrid systems. We point out the successes and limitations of the tool. The analysis procedure has been extended in a number of ways to address some of the tool's shortcomings. We evaluate these extensions, and conclude with some desiderata for verification tools for hybrid systems. AU - Henzinger, Thomas A AU - Preussig, Joerg AU - Wong Toi, Howard ID - 4475 SN - 0780370619 T2 - Proceedings of the 40th IEEE Conference on Decision and Control TI - Some lessons from the HYTECH experience VL - 3 ER - TY - GEN AB - Embedded software is software that interacts with physical processes. As em- bedded systems increasingly permeate our daily lives on all levels, from micros- copic devices to international networks, the cost-efficient development of reliable embedded software is one of the grand challenges in computer science today. The purpose of the workshop is to bring together researchers in all areas of computer science that are traditionally distinct but relevant to embedded software develop- ment, and to incubate a research community in this way. The workshop aims to cover all aspects of the design and implementation of embedded software, inclu- ding operating systems and middleware, programming languages and compilers, modeling and validation, software engineering and programming methodologies, scheduling and execution time analysis, networking and fault tolerance, as well as application areas, such as embedded control, real-time signal processing, and telecommunications. ED - Henzinger, Thomas A ID - 4449 SN - 9783540426738 TI - EMSOFT: Embedded Software VL - 2211 ER -