Automated performance and dependability evaluation using model checking

DOI10.1007/3-540-45798-4_12MaRDI QIDQ4411090zbMATH OpenFDO

Authors B. R. Haverkort, Holger Hermanns, Christel Baier, Joost-Pieter Katoen

Publication date 7 July 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2459/24590261.htm

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Performance evaluation := (process algebra + model checking) Markov chains
• Performability assessment by model checking of Markov reward models
• Specification techniques for Markov reward models
• A Markov chain model checker
• Model checking for performability

Cited in

(19)

• Assisting the design of a groupware system - Model checking usability aspects of thinkteam
• On the logical characterisation of performability properties
• Model checking for performability
• Using the Autodependogram in Model Diagnostic Checking
• Composite performance and dependability analysis
• Automated performance modeling of software generated by a design environment
• Formal methods for performance evaluation
• Markovian models for performance and dependability evaluation
• scientific article; zbMATH DE number 2155192 (Why is no real title available?)
• State-space support for path-based reward variables
• Performance evaluation with temporal rewards
• Performance evaluation := (process algebra + model checking) Markov chains
• scientific article; zbMATH DE number 2104633 (Why is no real title available?)
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference
• Specification techniques for Markov reward models
• Performance assessment and reliability analysis of dependable and distributed computing systems based on BDD and recursive merge
• Performability assessment by model checking of Markov reward models
• Mixing logics and rewards for the component-oriented specification of performance measures

Describes a project that uses

Uses Software

• SPIN
• GreatSPN
• GreatSPN 1.7
• PEPA

This page was built for publication: Automated performance and dependability evaluation using model checking

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