Integration of Analog and Discrete Synchronous Design
Second International Workshop on Hybrid Systems: Computation and Control, Nijmegen, Netherlands, March 1999, pages 193-208. LNCS 1569, Springer Verlag
© Springer Verlag
ABSTRACT
The synchronous family of languages (Lustre, Esterel, Signal, Statecharts) provide a great deal of support for verifying a control program at the design and compilation stage. However, a common aspect of embedded systems is that significant properties of the system can not be verified by formally analysing the controller (software) on its own. To analyse the system one requires to state and document assumptions on the environment. Furthermore, proving timeliness properties necessitates justifying a sampling interval and relating the synchronous step to metric time. Support for these activities is generally missing from current formal methods tools. In this paper we exploit simulation models - based on physical modelling of the environment - together with theorem proving, to prove properties of a closed loop system. We report on the work in progress on a case study provided by Saab Aerospace where deductive tools such as NP-Tools and simulation environments such as MATRIXx-SystemBuild are jointly used for verifying designs in Statecharts or programs in Lustre. The case study treats temperature and flow control in a climatic chamber.
Remarks:
The publishers have included a wrong figure (totally unrelated to this paper) in the printed volume. The version here includes the right figure.
| Related files: |
|---|
| HSCC.ps.gz | postscript document, compressed (with gzip) |
Copyright note for papers published by Springer Verlag:
I) Customer is authorized to conduct research for him-/herself and to copy a selection of the researched data (complete journals, individual articles of excerpts thereof) into its RAM.
II) Customer may only for his/her own use permanently store the data mentioned in paragraph i) and make hard copies thereof (downloading and printout). Springer-Verlag reserves the right to limit the extent and the number of copies and printouts in an appropriate manner. The transfer of the data in whole or in part - regardless of whether by electronic data carrier, remote data transmission or in the form of hard copies - as well as granting access to the stored data to third parties, the feeding of the data into the Intranet and commercial information brokerage are not permitted.
III) Translations, editing, arrangement, and other changes to the data and the public communication, representation or performance are prohibited.
[N99] Simin Nadjm-Tehrani, "Integration of Analog and Discrete Synchronous Design", Second International Workshop on Hybrid Systems: Computation and Control, Nijmegen, Netherlands, March 1999, pages 193-208. LNCS 1569, Springer Verlag |
