A state/event-based model-checking approach for the analysis of abstract system properties
From MaRDI portal
Publication:617925
DOI10.1016/j.scico.2010.07.002zbMath1213.68392OpenAlexW2123106596WikidataQ62047636 ScholiaQ62047636MaRDI QIDQ617925
Maurice H. ter Beek, Franco Mazzanti, Alessandro Fantechi, Stefania Gnesi
Publication date: 14 January 2011
Published in: Science of Computer Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.scico.2010.07.002
model checkingformal methodstemporal logicautomotive systemsstate machinesservice-oriented computingUML
Related Items
Model Checking Value-Passing Modal Specifications, A state/event-based model-checking approach for the analysis of abstract system properties, What Do Semantics Matter When the Meat Is Overcooked?, A formal model for service-oriented interactions, Intra- and interdiagram consistency checking of behavioral multiview models, Stepwise development and model checking of a distributed interlocking system using RAISE, A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting, Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints, A formal approach to the engineering of domain-specific distributed systems, From EU Projects to a Family of Model Checkers, Simulation for lattice-valued doubly labeled transition systems
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A state/event-based model-checking approach for the analysis of abstract system properties
- Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker
- ACTLW -- an action-based computation tree logic with unless operator
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Algebraic laws for nondeterminism and concurrency
- Three logics for branching bisimulation
- Temporal abstract interpretation
- Model Checking Software
