A Model-Checking Tool for Families of Services

International audience We propose a model-checking tool for on-the-fly verification of properties expressed in a branching-time temporal logic based on a deontic interpretation of classical modal and temporal operators over modal transition systems. We apply this tool to the analysis of variability...

Full description

Bibliographic Details
Main Authors: Asirelli, Patrizia, ter Beek, Maurice, H., Fantechi, Alessandro, Gnesi, Stefania
Other Authors: CNR Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo” Pisa (CNR, National Research Council of Italy, Università degli Studi di Firenze = University of Florence = Université de Florence (UniFI), Roberto Bruni, Juergen Dingel, TC 6, WG 6.1
Format: Conference Object
Language:English
Published: HAL CCSD 2011
Subjects:
[INFO]Computer Science [cs]
[INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI]
Iceland
Online Access:https://inria.hal.science/hal-01583318
https://inria.hal.science/hal-01583318/document
https://inria.hal.science/hal-01583318/file/978-3-642-21461-5_3_Chapter.pdf
https://doi.org/10.1007/978-3-642-21461-5_3
Description
Summary:International audience We propose a model-checking tool for on-the-fly verification of properties expressed in a branching-time temporal logic based on a deontic interpretation of classical modal and temporal operators over modal transition systems. We apply this tool to the analysis of variability in behavioural descriptions of families of services.

Similar Items