Combining theorem proving and continuous models in synchronous design
World Congress on Formal Methods, Tolouse, France, September 1999, Volume II, LNCS 1709, Springer Verlag, pages 1384-1399
© Springer Verlag
ABSTRACT
Support for system specification in terms of modelling and simulation environments has become a common practice in safety-critical applications. Also, a current trend is the automatic code-generation, and integration with formal methods tools in terms of translators from a high level design - often using common intermediate languages. What is missing from current formal methods tools is a well-founded integration of models for different parts of a system, being software/hardware or control-intensive/data-intensive. By hardware we mean here the full range of domains in engineering systems including mechanics, hydraulics, electronics. Thus, there is a methodological gap for proving system properties from semantically well-defined descriptions of the parts. We report on the progress achieved with the European SYRF project with regard to verification of integrated analog/discrete systems. The project pursues the development of new theories, application to case studies, and tool development in parallel. We use a ventilation control system, a case study provided by Saab Aerospace, to illustrate the work in progress on how hardware and software models used by engineers can be derived, composed and analysed for satisfaction of safety and timeliness properties.
| Related files: |
|---|
| FM99.pdf | Adobe Acrobat portable document |
| FM99.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.
[NA99] Simin Nadjm-Tehrani, Ove Akerlund, "Combining theorem proving and continuous models in synchronous design", World Congress on Formal Methods, Tolouse, France, September 1999, Volume II, LNCS 1709, Springer Verlag, pages 1384-1399 |
