Direct generation of invariants for reactive models

Autor: Ralph D. Jeffords, Constance L. Heitmeyer, Elizabeth I. Leonard, Myla Archer
Rok vydání: 2012
Předmět:
Zdroj: MEMOCODE
DOI: 10.1109/memcod.2012.6292308
Popis: Recently, software practitioners, using model-based engineering and similar methods, have begun developing software from models. After creating a model of the required system behavior, a developer can obtain assurance of the model by validating that it captures the intended behavior and verifying that it satisfies critical properties. Invariants are important to both validation, as a check that the model's behavior matches the intended behavior, and verification, as auxiliaries in proving critical system properties, either automatically or with human guidance. A common approach to discovering invariants is to propose and then check candidate invariants. In contrast, our invariant generation techniques deduce invariants directly from the specification of a model. This paper presents more powerful versions of our earlier techniques for invariant generation and illustrates their utility for a real-world AirLock system.
Databáze: OpenAIRE