A Two-Way Path Between Formal and Informal Design of Embedded Systems
| Autor: | Anders P. Ravn, Shuling Wang, Mengfei Yang, Mingshuai Chen, Naijun Zhan |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
0209 industrial biotechnology
Correctness Computer science business.industry Reliability (computer networking) Stateflow 0102 computer and information sciences 02 engineering and technology 01 natural sciences 020901 industrial engineering & automation 010201 computation theory & mathematics Hybrid system Embedded system Path (graph theory) Graphical model MATLAB business computer Formal verification computer.programming_language |
| Zdroj: | Unifying Theories of Programming ISBN: 9783319522272 UTP |
| DOI: | 10.1007/978-3-319-52228-9_4 |
| Popis: | It is well known that informal simulation-based design of embedded systems has a low initial cost and delivers early results; yet it cannot guarantee the correctness and reliability of the system to be developed. In contrast, the correctness and reliability of the system can be thoroughly investigated with formal design, but it requires a larger effort, which increases the development cost. Therefore, it is desirable for a designer to move between formal and informal design. This paper describes how to translate Hybrid CSP (HCSP) formal models into Simulink graphical models, so that the models can be simulated and tested using a MATLAB platform, thus avoiding expensive formal verification if the development is at a stage where it is considered unnecessary. Together with our previous work on encoding Simulink/Stateflow diagrams into HCSP, it provides a two-way path in the design of embedded systems, so that the designer can flexibly shift between formal and informal models. The translation from HCSP into Simulink diagrams is implemented as a fully automatic tool, and the correctness of the translation is justified using Unifying Theories of Programming (UTP). |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|