| dc.contributor.author | Kyas, Marcel | |
| dc.contributor.author | Hooman, Jozef | |
| dc.contributor.editor | Biel, Bettina | |
| dc.contributor.editor | Book, Matthias | |
| dc.contributor.editor | Gruhn, Volker | |
| dc.date.accessioned | 2019-08-13T08:27:56Z | |
| dc.date.available | 2019-08-13T08:27:56Z | |
| dc.date.issued | 2006 | |
| dc.identifier.isbn | 3-88579-173-0 | |
| dc.identifier.issn | 1617-5468 | |
| dc.identifier.uri | http://dl.gi.de/handle/20.500.12116/24307 | |
| dc.description.abstract | We present a general framework to support the compositional verification of timed systems using the interactive theorem prover PVS. The framework is based on timed traces that are an abstraction of the timed semantics of flat UML state machines. We define a compositional proof rule for parallel composition and prove its soundness in PVS. After composition, a hiding rule can be applied to hide internal events. The general theories have been applied to parts of the Medium Altitude Reconnaissance System (MARS) as deployed in the F-16 aircraft of the Royal Netherlands Air-Force. | en |
| dc.language.iso | en | |
| dc.publisher | Gesellschaft für Informatik e.V. | |
| dc.relation.ispartof | Software Engineering 2006, Proceedings der Fachtagung des GI-Fachbereichs Softwaretechnik | |
| dc.relation.ispartofseries | Lecture Notes in Informatics (LNI) - Proceedings, Volume P-79 | |
| dc.title | Compositional verification of timed components using PVS | en |
| dc.type | Text/Conference Paper | |
| dc.pubPlace | Bonn | |
| mci.reference.pages | 143-154 | |
| mci.conference.sessiontitle | Regular Research Papers | |
| mci.conference.location | Leipzig | |
| mci.conference.date | 28.-31. März 2006 | |
