Syspect -- Modelling, Specifying, and Verifying Real-Time Systems with Rich Data
    Download PDF
Johannes Fabe,Sven Linker,Ernst-Rudiger Olderog,Jan-David Quesel. Syspect -- Modelling, Specifying, and Verifying Real-Time Systems with Rich Data. International Journal of Software and Informatics, 2011,5(1-2Part1):117~137
Hits: 4216
Download times: 4572
Fund:This work was partially supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center "Automatic Verification and Analysis of Complex Systems" (SFB/TR 14 AVACS) and as part of the graduate school \TrustSoft" (GR
Abstract:We introduce the graphical tool Syspect for modelling, specifying, and automatically verifying reactive systems with continuous real-time constraints and complex, possibly infinite data. For modelling these systems, a UML profile comprising component diagrams, protocol state machines, and class diagrams is used; for specifying the formal semantics of these models, the combination CSP-OZ-DC of CSP (Communicating Sequential Processes), OZ (Object-Z) and DC (Duration Calculus) is employed; for verifying properties of these specifications, translators are provided to the input formats of the model checkers ARMC (Abstraction Refinement Model Checker) and SLAB (Slicing Abstraction model checker) as well as the tool H-PILoT (Hierarchical Proving by Instantiation in Local Theory extensions). The application of the tool is illustrated by a selection of examples that have been successfully analysed with Syspect.
keywords:real-time systems  modelling  UML  formal speciˉcation  CSP  Object-Z  Duration Calculus  model checking  abstraction-reˉnement  ARMC  SLAB  H-PILoT
View Full Text  View/Add Comment  Download reader

 

 

more>>  
Visitor:3139520
Top Paper  |  E-mail Alert  |  Publication Ethics  |  New Version

© Copyright by Institute of Software, the Chinese Academy of Sciences
京ICP备05046678号-5

京公网安备 11040202500065号