Composing model programs for analysis

DOI10.1016/j.jlap.2010.07.004zbMath1204.68133OpenAlexW2106340005MaRDI 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 analysismodel validationstate machinemodel-based testinglabeled transition systemmodel programscenario control

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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