Model-based Code Generation from CHARON



Model-based implementation of embedded software is a promising approach to improving reliability and development cost of embedded systems. Code generation is the last and the most challenging task of automatic synthesis of implementation from formal specification. We are studying various issues of transforming hybrid system models to digital programs, including platform-dependent adaptation and optimization, real time scheduling, and precise event detection. As a case study, we are implementing a CHARON-to-C++ code generator targeted to Sony’s quadruped robot dog, AIBO. Current implementation demonstrates that a simple CHARON specification in the form of a small set of differential equations is enough to describe complex behavior of robots such as getting up and down that would otherwise require tedious C++ programming to describe small amount of movement of every joint at every time step.




 



People

· Prof. Insup Lee

· Prof. Rajeev Alur

· Prof. Oleg Sokolsky

· Dr. Sebastian Fischmeister

· Madhukar Anand

·  Dr. Jesung Kim (Former Member)

·  Dr.Franjo Ivancic (Former Member)

Activities

Our current experimental platform consists of AIBO ERS-210A/N and a preliminary implementation of the code generator.

 




 

We are experimenting with CHARON models for various behavior of the dog, such as wagging the tail, tracking the ball, standing up, and so on. We are also interested in verifying whether the CHARON model is subject to invariant violations due to non-zero processing delay of the hardware platform that is not explicitly specified in the model. Currently, we are considering the predicate abstraction technique for the verification. Finally, we consider the problem of generating resource-aware code from hybrid system models that preserves the switching semantics of the model. Our approach starts by incorporating a resource model of the target platform into the hybrid systems model of the application. Code generation techniques are then applied to the integrated model to produce parameterized code. These parameters are specified at runtime by monitoring the state of the available resources. To guarantee the switching semantics of the model in the code, we have to ensure that there are no faulty or missed transitions. To prevent faulty transitions, we propose to instrument the guards and invariants for numerical and timing-induced errors. Insufficient sampling of instrumented guards can lead to missed transitions. To detect such a possibility, we develop a sufficient condition based on the periods of execution of the agents. This condition is used to build an algorithm that chooses optimal periods of execution so as to meet the resource constraints while providing semantic guarantees. We are currently working on an implementation of the proposed framework from hybrid systems models specified in CHARON.



Publications

Links