Specification and Seamless Verification ofEmbedded Real-Time Systems: FOCUS on Isabelle

Maria Spichkova

ISBN 10: 3836494523 / ISBN 13: 9783836494526

Edité par VDM Verlag Dr. M�ller 2008-04-15, 2008

A propos de cet article

N° de réf. du vendeur 6666-IUK-9783836494526

Détails bibliographiques

• Titre: Specification and Seamless Verification ofEmbedded Real-Time Systems: FOCUS on Isabelle
• Éditeur: VDM Verlag Dr. M�ller 2008-04-15
• Date de parution: 2008
• Langue: anglais
• ISBN à 10 chiffres: 3836494523
• ISBN à 13 chiffres: 9783836494526
• Reliure: Paperback
• État de l'article: New

A propos de ce titre

Synopsis

The purpose of this thesis is to create a coupling of the formal specification framework Focus in the generic theorem prover Isabelle/HOL, a logical framework based on Higher-Order Logic. The main focus of this work is on specification and verification of systems that are especially safety critical - embedded real-time systems. The specification and verification/validationmethodologies are treated as a single, joined, methodology with the main focus on the specification part.The key contributions of the thesis are+ Embedding of that part of the framework Focus, which is appropriate for the specification of real-time systems, into Isabelle/HOL. "Focus on Isabelle" enables to validate and verify system specificationsin a methodological way.+ Syntax extensions for Focus for the argumentation over time intervals: a special kind of tables, timed state transition diagrams, and a number of new operators. The deep embedding into Isabelle/HOL includes all these extensions.+ Schemata for automatic correctness proofs in Isabelle/HOL of the syntactic interfaces for specified system components.