Compositional Verification of Real-Time Applications

Autor:	Hooman, J.J.M., Roever, de, W.P., Langmaack, H., Pnueli, A.
Přispěvatelé:	Algorithms, Geometry and Applications
Rok vydání:	1998
Předmět:	Denotational semantics Theoretical computer science Basis (linear algebra) Computer science Formalism (philosophy) Hybrid system Real-time computing Verification system Focus (optics)
Zdroj:	Compositionality: The Significant Difference ISBN: 9783540654933 COMPOS Compositionality : The Significant Difference (Proceedings COMPOS'97, Bad Malente, Germany, September 1997; Revised Lectures), 276-300 STARTPAGE=276;ENDPAGE=300;TITLE=Compositionality : The Significant Difference (Proceedings COMPOS'97, Bad Malente, Germany, September 1997; Revised Lectures)
DOI:	10.1007/3-540-49213-5_10
Popis:	To support top-down design of distributed real-time systems, a framework of mixed terms has been incorporated in the verification system PVS. Programs and assertional specifications are treated in a uniform way. We focus on the timed behaviour of parallel composition and hiding, presenting several alternatives for the definition of a denotational semantics. This forms the basis of compositional proof rules for parallel composition and hiding. The formalism is applied to an example of a hybrid system, which also serves to illustrate our ideas on platform-independent programming.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d89e3541b968e3546095223302d5d917 https://doi.org/10.1007/3-540-49213-5_10 Zobrazit plný text záznamu