|
Overview
Objective
The project objective is to develop a methodology and toolkit for design of embedded software for multi-agent communicating hybrid systems. The methodology will cover various design stages, including modeling, simulation, analysis, implementation, and monitoring. The methodology will be based on formal modular and hierarchical semantics of multi-agent hybrid systems. The methodology will improve the process for hybrid systems design in several ways:
- decrease development costs through high-level modeling
- improve reusability by means of modular designs
- yield more reliable designs with the help of analysis and runtime valiadation.
Outline
Fulfilment of the objective involves the following tasks:
- To understand how to combine various features such as compositionality, hierarchy, concurrency, continuous flow, discrete steps, a modeling language for reactive hybrid systems is being developed. The rationale for the proposed language is to facilitate the development of embedded hybrid systems via high-level modeling and increased design automation. The language, called CHARON, will allow modular descriptions of communicating hybrid and hierarchic specification of control modes. The language will be given formal compositional semantics that facilitate the analysis of specifications.
- Design and implement a software toolkit that will provide support for the design of systems expressed in the new language. The toolkit will contain the following features and components:
- A compiler for the CHARON language, which will produce executable code in a target language, currently chosen to be Java.
- A simulator based on the operational semantics of the CHARON language.
- A graphical user interface that will tie all components of the toolkit together.
- Analysis tools for debugging the CHARON models by model checking or symbolic reachability analysis. The tools may output counterexamples as a feedback for the redesign when the requirements are violated.
- A tool for automatic generation of run-time checkers that allows the validation of an implementation.
- Establish the following theoretical results necessary to fulfil the above tasks:
- Compositional semantics for CHARON programs, which will be the basis for modular design and analysis.
- New simulation algorithms for the efficient and accurate detection and location of mode switching events. The simulation algorithms will be modular, exploiting the hierarchical mode structure to improve the efficiency of simulation by considering multiple time scales, and distributed, relying on the concurrency in designs.
- Compositional model checking algorithms that will allow the user to specify requirements in temporal logic, and efficiently verify the requirements against the system design by exploiting the modular structure of the design.
- Algorithms for the compositional, automatic synthesis of embedded hybrid systems.
- New theories are needed in order to propagate physical constraints from one layer of the hierarchy to another. Algorithms that abstract physical constraints depending on lower level constraints and task descriptions.
- Algorithms and proof rules for establishing consistency between different levels of abstraction and stepwise refinement of high-level specifications into more detailed designs.
- Algorithms and framework for relating high-level specifications to implementation details of distributed embedded systems and automatic generation of run-time checkers.
Accomplishments
Since the project start in May 2000, the UPenn team has performed the following tasks that contribute to the overall objective of the project.
- A preliminary version of the CHARON language has been designed. Informal semantics for CHARON have been completed and the work on formalisation of CHARON semantics is currently under way.
- A parser for the current version of CHARON has been implemented using JavaCC, a parser generation tool for Java. The grammar for CHARON is available on the project web site at http://www.cis.upenn.edu/mobies/charon/CHARONgrammar.html.
- An internal representation for CHARON programs, which will serve as the core of the CHARON design toolkit has been designed and implemented.
- A primitive simulator for CHARON programs is being implemented. Work on the modular simulator is currently in progress.
|
