The ABS modelling language targets concurrent and distributed object-oriented systems. The language has been designed to enable scalable formal verification of detailed executable models. This paper provides evidence for that claim: it gives formal specifications of safety properties in terms of histories of observable communication for ABS models as well as formal proofs of those properties. We illustrate our approach with a case study of a Network-on-Chip packet switching platform. We provide an executable formal model in ABS of a generic m × n mesh chip with an unbounded number of packets and verify several crucial properties. Our concern is formal verification of unbounded concurrent systems. In this paper we show how scalable verification can be achieved by compositional and local reasoning about history-based specifications of observable behavior.
CITATION STYLE
Din, C. C., Lizeth Tapia Tarifa, S., Hähnle, R., & Johnsen, E. B. (2015). History-based specification and verification of scalable concurrent and distributed systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9407, pp. 217–233). Springer Verlag. https://doi.org/10.1007/978-3-319-25423-4_14
Mendeley helps you to discover research relevant for your work.