liu.seSearch for publications in DiVA
Change search
ReferencesLink to record
Permanent link

Direct link
Combining theorem proving and continuous models in synchronous design
Linköping University, Department of Computer and Information Science, RTSLAB - Real-Time Systems Laboratory. Linköping University, The Institute of Technology.
Saab AB, Linköping, Sweden.
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)
Abstract [en]

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
Keyword [en]
control system, synchronous languages, theorem proving, hybrid system, proof methodology
Keyword [sv]
Toulouse 1999, Databehandling Systemutveckling.
National Category
Engineering and Technology
URN: 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: diva2:269264
Available from: 2009-10-11 Created: 2009-10-11 Last updated: 2014-03-25

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Nadjm-Tehrani, Simin
By organisation
RTSLAB - Real-Time Systems LaboratoryThe Institute of Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 23 hits
ReferencesLink to record
Permanent link

Direct link