Combining theorem proving and continuous models in synchronous design
1999 (English)In: FM’99 — Formal Methods: World Congress on Formal Methods in the Development of Computing Systems Toulouse, France, September 20–24, 1999 Proceedings, Volume II / [ed] Jeannette M. Wing, Jim Woodcock and Jim Davies, Berlin: Springer Berlin/Heidelberg, 1999, Vol. 1709, 1384-1399 p.Chapter in book (Refereed)
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.
Place, publisher, year, edition, pages
Berlin: Springer Berlin/Heidelberg, 1999. Vol. 1709, 1384-1399 p.
Lecture Notes in Computer Science, ISSN 0302-9743 (print), 1611-3349 (online) ; 1709
control system, synchronous languages, theorem proving, hybrid system, proof methodology
Toulouse 1999, Databehandling Systemutveckling.
Engineering and Technology
IdentifiersURN: urn:nbn:se:liu:diva-48368DOI: 10.1007/3-540-48118-4_23ISBN: 3-540-66588-9ISBN: 978-3-540-66588-5ISBN: e-978-3-540-48118-8OAI: oai:DiVA.org:liu-48368DiVA: diva2:269264