An action-based framework for veryfying logical and behavioural properties of concurrent systems

DOI10.1016/0169-7552(93)90047-8MaRDI QIDQ4697197zbMATH OpenOpenAlexFDO

Authors Rocco De Nicola, Alessandro Fantechi, S. Gnesi, Gioia Ristori

Publication date 29 June 1993

Published in Computer Networks and ISDN Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0169-7552(93)90047-8

zbMATH Keywords

process algebratemporal logicformal description techniquesbehavioural equivalencesconcurrent systemslabelled transition systembranching time logicverification environments

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Model checking for action-based logics
• scientific article; zbMATH DE number 4128366
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• scientific article; zbMATH DE number 5181778
• ACTLW -- an action-based computation tree logic with unless operator

Cited in

(16)

• Compositional specification in rewriting logic
• Automatic verification of distributed systems: the process algebra approach.
• ACTLW -- an action-based computation tree logic with unless operator
• Model checking for action-based logics
• Folk Theorems on the Correspondence between State-Based and Event-Based Systems
• Towards the assessment of logics for concurrent actions
• ACTL for modal interface automata
• Verification and refinement with fine-grained action-based concurrent objects
• scientific article; zbMATH DE number 4128366 (Why is no real title available?)
• Assisting requirement formalization by means of natural language translation
• Encoding safety in \(\mathrm{CLL}_R\)
• Compositional verification of asynchronous concurrent systems using CADP
• Compositionality and bisimulation: A negative result
• Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking
• Model checking mobile ad hoc networks
• Model checking fuzzy computation tree logic

Describes a project that uses

Uses Software

• AUTO

This page was built for publication: An action-based framework for veryfying logical and behavioural properties of concurrent systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4697197)