Zobacz książki o podobnej tematyce

Więcej informacji o Specification and Seamless Verification of Embedded Real-Time Systems - FOCUS on Isabelle

• Dane szczegółowe
• Opis
• Ulubione w innej kategorii

Za ten zakup dostaniesz 219 punkty

Opis

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/validation§methodologies 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 specifications§in 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.

Szczegóły książki

Kategoria Knihy po anglicky Technology, engineering, agriculture Technology: general issues Engineering: general

• Pełny tytuł: Specification and Seamless Verification of Embedded Real-Time Systems - FOCUS on Isabelle
• Autor: Maria Spichkova
• Język: Angielski
• Oprawa: Miękka
• Liczba stron: 292
• EAN: 9783836494526
• ISBN: 3836494523
• ID: 07093264
• Wydawca: VDM Verlag Dr. Mueller E.K.
• Waga: 395 g
• Wymiary: 229 × 152 × 15 mm
• Data wydania: 17. April 2008

Ulubione w innej kategorii

---

---

---