Formal Verification of UML Statecharts with Real-Time Extensions
| Autor: | Alexandre David, Wang Yi, M. Oliver Möller |
|---|---|
| Rok vydání: | 2002 |
| Předmět: |
Model checking
Computation tree logic computer.internet_protocol Computer science Programming language Computer Science::Software Engineering Deadlock computer.software_genre Operational semantics UML state machine Formal grammar Unified Modeling Language State diagram Formal verification computer Algorithm XML computer.programming_language |
| Zdroj: | Fundamental Approaches to Software Engineering ISBN: 9783540433538 FASE |
| Popis: | We present a framework for formal verification of a real-time extension of UML statecharts. For clarity, we restrict ourselves to a reasonable subset of the rich UML statechart model and extend this with real-time constructs (clocks, timed guards, and invariants). We equip the obtained formalism, called hierarchical timed automata (HTA), with an operational semantics. We outline a translation of one HTA to a network of flat timed automata, that can serve as input to the real-time model checking tool UPPAAL. This translation can be used to faithfully verify deadlock-freedom, safety, and unbounded response properties of the HTA model. We report on an XML-based implementation of this translation, use the well-known pacemaker example to illustrate our technique, and report run-time data for the formal verification part. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|