PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Gnesi S. Families of dependable systems:a model checking approach. Broy M., Peled D., Kalus G. (NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 34). Amsterdam: IOS Press, 2013.
 
 
Abstract
(English)
A number of models, logics and associated tools for the qualitative analysis of variability aspects and their use to deal with adaptability and evolvability of systems have recently been proposed. In these lectures, we will introduce the action-based branching-time temporal logic MHML which allows expressing constraints over the products of a family as well as constraints over their behaviour in a single logical framework. Based on model-checking techniques for MHML, a modelling and verification framework will be presented that can automatically generate all the valid productsof the family, visualise the family/products behaviour and efficiently model check properties expressed in MHML over products and families alike. The use of the above methods, techniques and tools will be applied to a scenario derived from a family of dependable systems.
URL: http://www.iospress.nl/book/engineering-dependable-software-systems/
Subject Model checking
Temporal logics
Product lines
D.2.4 Software/Program Verification


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional