Description| People| Publications
Description
MOQS (Modeling and Analysis of QoS for Component-Based Designs) is a research project supported by the Netherlands Foundation for Scientific Research (NWO). It aims to develop a theory, tools and techniques for the specification and analysis of Quality of Service (QoS) for component-based designs.
Component-based design is widely considered as an important approach to develop systems in a time and cost effective way. A challenge is to predict the global system properties from local component properties, especially for extra-functional requirements such as quality of service (QoS), resource consumption and responsiveness. The goal of this project is to develop methods and tools for the design time analysis of QoS properties of component-based systems. Since QoS properties are usually stochastic in nature, we base our techniques on stochastic modeling and analysis methods. In particular, we plan to devise a notion of stochastic interface automaton. Such automata summarize the QoS properties of a system component by specifying the QoS requirements the component needs from its environment and the QoS guarantees it provides. To verify the compliance of a component with its interface specification, we seek to extend model checking, abstraction and model-based testing techniques that exist for stochastic systems to these interface automata. We plan to integrate these techniques into a tool environment based on the existing tools TorX, Modest/Motor and ETMCC.
People
Current participants of MOQS project:
- prof.dr. Ed Brinksma
- prof.dr.ir Boudewijn Haverkort
- prof.dr.ir. Joost-Pieter Katoen
- dr. Marielle Stoelinga
- dr. Hichem Boudali
- dr. Lucia Cloth
- Andre Nijmeijer
Publications
- .
Arcade - A Formal, Extensible, Model-based Dependability Evaluation Framework.
In: Proceedings of the 3rd International IEEE UML/AADL Workshop
- . A Testing Scenario for Probabilistic Processes. In: Journal of the ACM 2007
- .
How Fast and Fat Is Your Probabilistic Model Checker? an experimental performance comparison.
In: Proceedings of HVC'07 Note: to appear
- . CORAL - a tool for COmpositional Reliability and Availability anaLysis. In: ARTIST workshop: Tool Platforms for Embedded Systems Modeling, Analysis and Validation.
- . Model Checking Markov Chains with Actions and State Labels. In: forthcoming in IEEE TSE, 2007
- .
CSL model checking algorithms for QBDs. In: Theoretical Computer Science
(volume 382, pages 24--41), 2007 Note: doi:10.1016/j.tcs.2007.05.007
- .
A Centralized Feedback Control Model for Resource Management in Wireless Networks.
In: Proceedings og the 8th International Workshop on Performability Modeling of Computer
and Communication Systems (PMCCS 2007), 2007 Note: to appear
- .
Best of Three Worlds: Towards Sounds Architectural Dependability Models.
In: Proceedings og the 8th International Workshop on Performability Modeling of Computer
and Communication Systems (PMCCS 2007), 2007 Note: to appear
- . Game Relations and Metrics. In: LICS '07: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science (pages 99--108), IEEE Computer Society, 2007
- . A Compositional Semantics for Dynamic Fault Tree Analysis in terms of Interactive Markov Chains. In: Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA'07) (pages 708-717), LNCS, Springer, 2007
- .
Computing Battery Lifetime Distributions.
In: Proceedings of the 37th International Conference on Dependable Systems and Networks
(DSN'07) (pages 780-789), 2007 Note: doi:10.1109/DSN.2007.26
- . Dynamic Fault Tree Analysis Using Input/Output Interactive Markov Chains. In: The 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2007, UK, Proceedings (pages 708-717), IEEE Computer Society, 2007
- . Quantitative Compositional Reasoning. In: Proceedings of QEST, 2006
- . A Semantic Framework for Test Coverage. In: Proceedings ATVA, 2006
- . A Versatile Infinite-State Markov Reward Model to Study Bottlenecks in 2-Hop Ad Hoc Networks. In: Proceedings of QEST, 2006
- . Five Performability Algorithms: A Comparison. In: Proceedings Markov Anniversary Meeting, 2006