Checking formal specifications under simulation
- 22 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10636404,p. 455-460
- https://doi.org/10.1109/iccd.1997.628908
Abstract
"Verification" of large multiprocessor designs currently heavily on simulation. Formal techniques such as model checking are typically only applied to small parts of the system, due to issues of computational and notational complexity. With these two facts in mind the authors have designed a platform which aims to help bridge the gap between formal verification and simulation. They present a temporal logic specification language which includes constructs for specifying system behavior at a high level of abstraction, and discuss its use in simulation and model checking.Keywords
This publication has 3 references indexed in Scilit:
- The temporal logic of actionsACM Transactions on Programming Languages and Systems, 1994
- The Temporal Logic of Reactive and Concurrent SystemsPublished by Springer Nature ,1992
- Deciding full branching time logicInformation and Control, 1984