Loading...
Please wait, while we are loading the content...
Similar Documents
Electronic Communications of the EASST Volume 23 ( 2009 ) Proceedings of the Ninth International Workshop on Automated Verification of Critical Systems ( AVOCS 2009 ) Towards SMV Model Checking of S IGNAL ( multi-clocked ) Specifications
| Content Provider | Semantic Scholar |
|---|---|
| Author | Peralta, Julio C. Gautier, Thierry |
| Copyright Year | 2009 |
| Abstract | SIGNAL is a high-level data-flow specification language that equall y allows multi-clocked descriptions as well as single-clock ed ones. It has a formal semantics and is supported by several formal tools for simulat ion and static validation. This generality renders it useful for various specification , simulation, and verification tasks in embedded system design. SMV, in turn, is a langu ge and model checker where synchronous models are single-clocked by defi nition. Roughly, we use standard techniques to describe clocks by Boolean varia bles, with the advantage that the number of such variables is kept to a minimum through a static analysis provided by the SIGNAL compiler. In particular, we propose a translation from poss ibly multi-clocked SIGNAL specifications into SMV specifications for their correspond ing verification by model checking. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | https://journal.ub.tu-berlin.de/eceasst/article/download/308/299 |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
