Composing model programs for analysis

DOI10.1016/j.jlap.2010.07.004zbMath1204.68133MaRDI QIDQ710670

Margus Veanes, Jonathan Jacky

Publication date: 22 October 2010

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2010.07.004

zbMATH Keywords

model analysis; model validation; state machine; model-based testing; labeled transition system; model program; scenario control

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Uses Software

• z3
• NModel
• SpecExplorer

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Partial updates
• Formal techniques for networked and distributed systems -- FORTE 2008. 28th IFIP WG 6.1 international conference Tokyo, Japan, June 10--13, 2008. Proceedings
• Testing of software and communication systems. 21st IFIP WG 6.1 international conference, TESTCOM 2009 and 9th international workshop, FATES 2009, Eindhoven, The Netherlands, November 2--4, 2009. Proceedings
• Defining conditional independence using collapses
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Logics of specification languages
• Input-Output Model Programs
• Symbolic Bounded Conformance Checking of Model Programs
• The Composition of Event-B Models
• State Isomorphism in Model Programs with Abstract Data Structures
• Composition of Model Programs
• Formal verification of parallel programs
• The B-Book
• Evolving Algebras 1993: Lipari Guide
• Dynamic partial-order reduction for model checking software
• Verification: Theory and Practice
• Model-Based Software Testing and Analysis with C#
• On Bounded Reachability of Programs with Set Comprehensions
• FM 2005: Formal Methods