Advertisement
Published in:
2007 | OriginalPaper | Chapter
Verifying Temporal Properties of CommUnity Designs
Authors : Nazareno Aguirre, Germán Regis, Tom Maibaum
Published in: Integrated Formal Methods
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We study the use of some verification techniques for reasoning about temporal properties of CommUnity designs. We concentrate on the verification of temporal properties in the context of branching-time temporal logic using the SMV tool.
We also discuss ways of modularising the temporal reasoning, by exploiting the various kinds of morphisms between designs available in CommUnity. Moreover, we combine SMV verification with some abstract interpretation mechanisms to overcome a limitation, with respect to the use of structure for simplification of verification, of CommUnity’s refinement morphisms, the lack of support for data refinement.