direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments


Machine Checkable Timed CSP
Zitatschlüssel goethel09machine
Autor Thomas Göthel and Sabine Glesner
Buchtitel Proc. of The First NASA Formal Methods Symposium (NFM '09)
Seiten pp.126–135
Jahr 2009
Verlag NASA Conference Publication
Zusammenfassung The correctness of safety-critical embedded software is crucial, whereas non-functional properties like deadlock-freedom and real-time constraints are particularly important. The real-time calculus Timed CSP is capable of expressing such properties and can therefore be used to verify embedded software. In this paper, we present our formalization of Timed CSP in the Isabelle/HOL theorem prover, which we have formulated as an operational coalgebraic semantics together with bisimulation equivalences and coalgebraic invariants. Furthermore, we apply these techniques in an abstract specification with real-time constraints, which is the basis for current work in which we verify the components of a simple real-time operating system deployed on a satellite.
Typ der Publikation Conference Article
Download Bibtex Eintrag

Zusatzinformationen / Extras


Schnellnavigation zur Seite über Nummerneingabe