Early Verification of Computer Systems Temporal Properties
| Autor: | Paulo Sérgio Muniz Silva |
|---|---|
| Rok vydání: | 2005 |
| Předmět: |
Interpretation (logic)
Theoretical computer science Functional verification message sequence chart temporal reasoning General Computer Science Computer science Runtime verification Message sequence chart System behavior verification Theoretical Computer Science Metric (mathematics) Formal verification Time complexity Computer Science(all) |
| Zdroj: | Electronic Notes in Theoretical Computer Science. 130:211-233 |
| ISSN: | 1571-0661 |
| DOI: | 10.1016/j.entcs.2005.03.012 |
| Popis: | In early moments of computer systems development, computer engineers typically draw interaction diagrams, occasionally annotated with timing constraints, to reason about the specification of the system behavior. One of the most popular of these diagrams is the Message Sequence Chart (MSC). However, not always does the intended behavior described by MSCs correspond to their actual behavior. To help the formal verification of their actual behavior, i.e. their temporal properties, this paper describes an interpretation of basic timed MSCs in a temporal framework that formally represents, in a unified model, both the qualitative and the metric temporal information conveyed in these intuitive diagrams. The framework solves the verification problems in polynomial time and lays the foundation of an automatic tool. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect