Design and verification of systems with exogenous coordination using vereofy
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
Contributors
Abstract
The feasibility of formal methods for the analysis of complex systems crucially depends on a modeling framework that supports compositional design, stepwise refinement and abstractions. An important feature is the clear separation of coordination and computation which permits to apply various verification techniques for the computation performed by components and interactions as well as dependencies between the components. We report here on a model-checking approach using the tool Vereofy that is based on an exogenous coordination model, where the components are represented by their behavioral interfaces. Vereofy supports the verification of the components and their communication structure. Our approach is illustrated by means of a case study with a sensor network where Vereofy has been used to establish several properties of the sensor nodes and their routing procedures.
Details
Original language | English |
---|---|
Title of host publication | Leveraging Applications of Formal Methods, Verification, and Validation - 4th International Symposium on Leveraging Applications, ISoLA 2010, Proceedings |
Pages | 97-111 |
Number of pages | 15 |
Edition | PART 2 |
Publication status | Published - 2010 |
Peer-reviewed | Yes |
Publication series
Series | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Number | PART 2 |
Volume | 6416 LNCS |
ISSN | 0302-9743 |
Conference
Title | 4th International Symposium on Leveraging Applications, ISoLA 2010 |
---|---|
Duration | 18 - 21 October 2010 |
City | Heraklion, Crete |
Country | Greece |
External IDs
ORCID | /0000-0002-5321-9343/work/173985300 |
---|---|
ORCID | /0000-0003-1724-2586/work/173988430 |