|Formal Methods & Tools|
pecification-based erformbility hcking
SPACE (Specification-based PerformAbility ChEcking) is a research project supported by the Netherlands Foundation for Scientific Research (NWO). It aims at the development of a coherent framework to facilitate the integration of performability analysis into the design process.
For modern fault-tolerant and distributed computer and communication systems, the assessment of performance and dependability (i.e., performability) is of crucial importance. Their complexity makes the prediction of their performability impossible by engineering ``rules of thumbs''. In addition, due to the increasing dependence of society on such systems, a mismatch between the required and the offered performability level can have widespread impact. Therefore, the desire of integrating performability assessment into the design trajectory is steadily increasing.
This proposal aims at the development of a coherent framework to facilitate the integration of performability analysis into the design process. The goal is to develop methods, techniques and prototypical software tools for the specification and automated analysis of performability measures of interest, and to apply these developed means to case studies of representative complexity. We intend to focus on the development of
Concretely, we plan to extend our recently developed model-checking approach for pure performance measures towards performability measures and to develop techniques to combat the state-space explosion problem based on the measure-of-interest driven model-generation.
- a specification formalism for performability measures at a high level of abstraction, and on the design and
- implementation of efficient verification algorithms for the assessment of such measures.
Project description in postscript and pdf formats.
PeopleCurrent participants of the SPACE project:
SPACE logo design © Holger Hermanns
Updated on December 2, 2002