Assisting the design of a groupware system - Model checking usability aspects of thinkteam

DOI10.1016/j.jlap.2008.11.004zbMath1183.68363OpenAlexW2070505997MaRDI QIDQ1014561

Mieke Massink, Gianluca Trentanni, Diego Latella, Maurizio Sebastianis, Maurice H. ter Beek, Stefania Gnesi

Publication date: 29 April 2009

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.2008.11.004

zbMATH Keywords

verificationmodel checkingformal methodsconcurrencygroupware

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• PRISM
• SPIN
• SPSS
• SAS
• COWS
• MarCaSPiS
• KLAIM
• GroupKit

Cites Work

• A survey of retrial queues
• Model checking mobile stochastic logic
• Model-checking large structured Markov chains.
• Comparative branching-time semantics for Markov chains
• On the verification of qualitative properties of probabilistic processes under fairness constraints.
• MarCaSPiS: a Markovian Extension of a Calculus for Services
• An Extended Temporal Logic for CSCW
• Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Retrial Queues
• Model-checking continuous-time Markov chains
• A Calculus for Orchestration of Web Services
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item