Using a symbolic model checker for verify safety properties in SA/RT models
| Author | |
|---|---|
| Abstract |
In this paper, structured methods are integrated with formal verification methods based on temporal logic. The goal is to use an operational method (SA/RT) for the system behavioural specification, and to complement this with safety properties expressed in a declarative style using temporal logic (CTL). These properties are checked against the operational specification using a model checker (SMV).
|
| Year of Publication |
1995
|
| Publisher |
Springer Berlin Heidelberg
|
| Conference Location |
Berlin, Heidelberg
|
| ISBN Number |
978-3-540-45552-3
|
| Download citation | |
| Number of Pages |
59-75
|