Paper Info
Title
History-Based Specification and Verification of Scalable Concurrent and Distributed Systems.
Abstract
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 times 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.
Year
Venue
Field
2015
ICFEM
Intelligent verification,Computer science,Network packet,Formal specification,Mathematical proof,Packet switching,Formal verification,Scalability,Executable,Distributed computing
DocType
Citations 
PageRank 
Conference
7
0.45
References 
Authors
26
4
Name
Order
Citations
PageRank
Crystal Chang Din1827.87
S. Lizeth Tapia Tarifa214711.07
Reiner Hähnle31272106.50
Einar Broch Johnsen4107169.56