2006
Software
Metadata Only Access
UMC V3.3
Mazzanti F
Strumento sofware per la modellazzione e la verifica formale (model checking) di sistemi concorrenti descritti tarmite statecharts.
Mazzanti F
Strumento sofware per la modellazzione e la verifica formale (model checking) di sistemi concorrenti descritti tarmite statecharts.
See at:
CNR IRIS 
2006
Software
Metadata Only Access
COWS V0.2
Mazzanti F
Strumento sofware per la simulazione di sistemi descritti tramite l'algebra di processo COWS.
Mazzanti F
Strumento sofware per la simulazione di sistemi descritti tramite l'algebra di processo COWS.
See at:
CNR IRIS
2006
Software
Metadata Only Access
PSC V0.4
Franco Mazzanti
Strumento software per la simulazione di sistemi descritti tramite l'algebra di processo PSC.
Franco Mazzanti
Strumento software per la simulazione di sistemi descritti tramite l'algebra di processo PSC.
See at:
CNR IRIS
2007
Software
Restricted
CMC: COWS model checker version 0.4
Mazzanti F
Model checker prototipale per il linguaggio di specifica COWS, sviluppato nell'ambito del progetto Sensoria
Mazzanti F
Model checker prototipale per il linguaggio di specifica COWS, sviluppato nell'ambito del progetto Sensoria
2008
Software
Metadata Only Access
See at:
CNR IRIS
2003
Other
Open Access
UMC User Guide (version 2.5)
Mazzanti F
In this paper we describe in detail the functionalities of UMC, a new tool for the exploration, analisys and on-the-fly model checking of the dynamic behaviour of UML models. Models are described as collections of communicating objects. Objects belong to classes, whose dynamic behaviour is described by statecharts. The logic supported by the tool is an extension of mu-ACTL and has the power of full mu-calculus.
Mazzanti F
In this paper we describe in detail the functionalities of UMC, a new tool for the exploration, analisys and on-the-fly model checking of the dynamic behaviour of UML models. Models are described as collections of communicating objects. Objects belong to classes, whose dynamic behaviour is described by statecharts. The logic supported by the tool is an extension of mu-ACTL and has the power of full mu-calculus.
See at:
CNR IRIS 
| ISTI Repository | CNR IRIS
2006
Other
Open Access
UMC User Guide (version 3.3)
Mazzanti F
In this report we present the prototypical UMC verification tool under development at ISTI. UMC accept a system specification given in UML-like style as a collection of active objects, modelled by state-machines, and whose behavior is described through statecharts. On such systems UMC allows to verify properties specified in the mu-UCTL logic: a temporal logic which enriches the full mu-calculus with the more abstract (and weak) CTL/ACTL like temporal operators, and with a rich set of state propositions and ACTL action expressions. Both the basic comand-line oriented tool (umc) and its more user-friendly web-based interface are presented. This web interface integrates also verification functionalities provided by the other environments (EST, FC2TOOLS) which allow system abstraction and minimization.
Mazzanti F
In this report we present the prototypical UMC verification tool under development at ISTI. UMC accept a system specification given in UML-like style as a collection of active objects, modelled by state-machines, and whose behavior is described through statecharts. On such systems UMC allows to verify properties specified in the mu-UCTL logic: a temporal logic which enriches the full mu-calculus with the more abstract (and weak) CTL/ACTL like temporal operators, and with a rich set of state propositions and ACTL action expressions. Both the basic comand-line oriented tool (umc) and its more user-friendly web-based interface are presented. This web interface integrates also verification functionalities provided by the other environments (EST, FC2TOOLS) which allow system abstraction and minimization.
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2006
Other
Open Access
SENSORIA - D3.3A - An Overview of Techniques for Behavioural Properties
Caires L, Zawbocki A, Corradini A, Mazzanti F, Loreti M, Nielson H R
The main goal of WP3 is to coordinate the partners efforts towards the development of qualitative analysis methods for global services. In particular, this deliverable reports on the research activity carried on during the first 12 months by the SENSORIA partners in the advancement of the state of art for a wide spectrum of techniques suitable for the description and analysis of the behavioral properties of services. Twelve original contributions have emerged as result of this research activity. In the following sections of this document an overview is given of the performed activity and the results are described with a limited level of technical details . The full details of the contributions can be found in the twelve papers mentioned in the final "Relevant Sensoria Publications and Reports" Section.
Caires L, Zawbocki A, Corradini A, Mazzanti F, Loreti M, Nielson H R
The main goal of WP3 is to coordinate the partners efforts towards the development of qualitative analysis methods for global services. In particular, this deliverable reports on the research activity carried on during the first 12 months by the SENSORIA partners in the advancement of the state of art for a wide spectrum of techniques suitable for the description and analysis of the behavioral properties of services. Twelve original contributions have emerged as result of this research activity. In the following sections of this document an overview is given of the performed activity and the results are described with a limited level of technical details . The full details of the contributions can be found in the twelve papers mentioned in the final "Relevant Sensoria Publications and Reports" Section.
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2009
Other
Open Access
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2011
Conference article
Restricted
Design and validation of variability in product lines
Asirelli P Ter Beek M H, Fantechi A, Gnesi S, Mazzanti F
We propose an emerging solution technique, pushing the application of model-checking techniques to the design and validation of variability in a product line (PL), mainly aimed at those industrial domains where model-based development is adopted for the development of safety-critical systems.
Asirelli P Ter Beek M H, Fantechi A, Gnesi S, Mazzanti F
We propose an emerging solution technique, pushing the application of model-checking techniques to the design and validation of variability in a product line (PL), mainly aimed at those industrial domains where model-based development is adopted for the development of safety-critical systems.
2011
Contribution to book
Restricted
Tools and Verification
Bartoletti M, Caires L, Lanese I, Mazzanti F, Sangiorgi D, Vieira H T, Zunino R
This chapter presents different tools that have been developed inside the Sensoria project. Sensoria studied qualitative analysis techniques for verifying properties of service implementations with respect to their formal specifications. The tools presented in this chapter have been developed to carry out the analysis in an automated, or semi-automated, way. We present four different tools, all developed during the Sensoria project, exploiting new techniques and calculi from the Sensoria project itself.Project(s): Software Engineering for Service-Oriented Overlay Computers
Bartoletti M, Caires L, Lanese I, Mazzanti F, Sangiorgi D, Vieira H T, Zunino R
This chapter presents different tools that have been developed inside the Sensoria project. Sensoria studied qualitative analysis techniques for verifying properties of service implementations with respect to their formal specifications. The tools presented in this chapter have been developed to carry out the analysis in an automated, or semi-automated, way. We present four different tools, all developed during the Sensoria project, exploiting new techniques and calculi from the Sensoria project itself.Project(s): Software Engineering for Service-Oriented Overlay Computers
See at:
CNR IRIS | CNR IRIS | link.springer.com
1995
Other
Open Access
Formalising a software safety case via belief networks
Delic K, Mazzanti F, Strigini L
Belief Networks (also known as Graphical Probabilistic Networks and with various other names) offer a useful fonnallanguage for stating complex arguments in rigorous, yet visually clear terms. They are thus promising candidates for describing the complex, often unclear reasoning that is often implied, but not described, when reasoning about software dependability, in particular when "engineering judgement" comes into play. We introduce the problem of building a rigorous safety case for software, and argue the merits of belief networks as an aid for building, criticising and perfecting such safety cases. This first report includes a high-level introduction to Belief Networks, and then introduces and discusses a small but realistic example. Our conclusion is that this method has great potential for making safety arguments easier to communicate and check, and in the end more trustworthy.
Delic K, Mazzanti F, Strigini L
Belief Networks (also known as Graphical Probabilistic Networks and with various other names) offer a useful fonnallanguage for stating complex arguments in rigorous, yet visually clear terms. They are thus promising candidates for describing the complex, often unclear reasoning that is often implied, but not described, when reasoning about software dependability, in particular when "engineering judgement" comes into play. We introduce the problem of building a rigorous safety case for software, and argue the merits of belief networks as an aid for building, criticising and perfecting such safety cases. This first report includes a high-level introduction to Belief Networks, and then introduces and discusses a small but realistic example. Our conclusion is that this method has great potential for making safety arguments easier to communicate and check, and in the end more trustworthy.
1997
Other
Metadata Only Access
Guide to erroneous executions in Ada 95
Mazzanti F
We present a detailed analysis of the possible ways in which the execution of an Ada 95 program might become totally unpredictable. In particular, we discuss those language aspects which allow a program execution to become erroneous or which have an undefined semantics. The Ada 95 language definition is assessed with respect to its completeness and clarity in presenting these aspects. The evolution of these aspects from Ada 83 to Ada 95 is summarised
Mazzanti F
We present a detailed analysis of the possible ways in which the execution of an Ada 95 program might become totally unpredictable. In particular, we discuss those language aspects which allow a program execution to become erroneous or which have an undefined semantics. The Ada 95 language definition is assessed with respect to its completeness and clarity in presenting these aspects. The evolution of these aspects from Ada 83 to Ada 95 is summarised
See at:
CNR IRIS
1994
Other
Open Access
A software engineering framework for software safety claims
Mazzanti F
This document is intended to contribute to the development of the SHIP safety case by presenting a possible line of reasoning for the organization of software safety claims. Sections from 3 to 6 aim at the illustration of a generic picture of the expectable difficulties in the development of correct software and related solutions (Section 6 is the one which probably needs more work). Initially, drawing this general picture was the main goal of this report. During this writing, it has become evident that a design of a full picture including an evaluation of the effectiveness of all the mentioned methodologies is a too complex task. Therefore, while preserving its usefulness as a global refernce schema, this picture should not be expected to produce usable numerical inputs for the evaluation of the transition probabilities in the SHIP safety case. Section 7, which is probably the most interesting from the SHIP point of view, investigates a possible way to formally structure and organize the reasonaing. This part is still in an extremely draft form, and will be improved in the next months. The overall English style (sorry for the current one) also will be revised.
Mazzanti F
This document is intended to contribute to the development of the SHIP safety case by presenting a possible line of reasoning for the organization of software safety claims. Sections from 3 to 6 aim at the illustration of a generic picture of the expectable difficulties in the development of correct software and related solutions (Section 6 is the one which probably needs more work). Initially, drawing this general picture was the main goal of this report. During this writing, it has become evident that a design of a full picture including an evaluation of the effectiveness of all the mentioned methodologies is a too complex task. Therefore, while preserving its usefulness as a global refernce schema, this picture should not be expected to produce usable numerical inputs for the evaluation of the transition probabilities in the SHIP safety case. Section 7, which is probably the most interesting from the SHIP point of view, investigates a possible way to formally structure and organize the reasonaing. This part is still in an extremely draft form, and will be improved in the next months. The overall English style (sorry for the current one) also will be revised.
1996
Other
Open Access
Towards the static detection of erroneus executions in Ada 95
Marzullo C, Mazzanti F
Being absolutely certain that a program execution will not result in unpredictable behaviour is very difficult. Although there is no way to avoid the underlying theoretical difficulties, we believe that a human-centered approach in exploiting advanced static analysis techniques is a viable solution. This paper presents some preliminary results of a feasibility study on this subject, which is currently underway at the I.E.I.
Marzullo C, Mazzanti F
Being absolutely certain that a program execution will not result in unpredictable behaviour is very difficult. Although there is no way to avoid the underlying theoretical difficulties, we believe that a human-centered approach in exploiting advanced static analysis techniques is a viable solution. This paper presents some preliminary results of a feasibility study on this subject, which is currently underway at the I.E.I.
1997
Conference article
Restricted
Formalising engineering judgement on software dependability via belief networks
Delic K, Mazzanti F, Strigini L
We present the use of Bayesian belief networks to formalise reasoning about software dependability, so as to make assessments easier to build and to check. Bayesian belief networks include a graphical representation of the structure of a complex argument, and a sound calculus for representing probabilistic information and updating it with new observations. We illustrate the method and show its feasibility via a simple example, developed via a commercial computer tool, representing a form of argument which is often used in claims for high dependability. This example is not meant to be "typical", since a sound and complete argument can only be built using the knowledge available in the specific case of interest. Although the modelled scenario is rather simple, but it demonstrates the advantages of using belief networks for sounder assessment of reliability and safety.
Delic K, Mazzanti F, Strigini L
We present the use of Bayesian belief networks to formalise reasoning about software dependability, so as to make assessments easier to build and to check. Bayesian belief networks include a graphical representation of the structure of a complex argument, and a sound calculus for representing probabilistic information and updating it with new observations. We illustrate the method and show its feasibility via a simple example, developed via a commercial computer tool, representing a form of argument which is often used in claims for high dependability. This example is not meant to be "typical", since a sound and complete argument can only be built using the knowledge available in the specific case of interest. Although the modelled scenario is rather simple, but it demonstrates the advantages of using belief networks for sounder assessment of reliability and safety.
1995
Conference article
Restricted
Coding regulations for safety critical software development
Mazzanti F
This paper presents some limits and irregularities in current standards for safety critical software development, and suggests ways to improve the state of the art. The need for well organized, rigorous and verifiable coding regulations to promote the development of software with predictable quality and safety characteristics is explained. We show specific examples of weaknesses in standards and make proposals for improvement.
Mazzanti F
This paper presents some limits and irregularities in current standards for safety critical software development, and suggests ways to improve the state of the art. The need for well organized, rigorous and verifiable coding regulations to promote the development of software with predictable quality and safety characteristics is explained. We show specific examples of weaknesses in standards and make proposals for improvement.
See at:
CNR IRIS | CNR IRIS | www.scopus.com
1996
Conference article
Restricted
Towards the static detection of erroneus executions in Ada 95
Mazzanti F, Marzullo C
Being absolutely certain that a program execution will not result in unpredictable behaviour is very difficult. Although there is no way to avoid the underlying theoretical difficulties, we believe that a human-centered approach in exploiting advanced static analysis techniques is a viable solution. This paper presents some preliminary results of a feasibility study on this subject, which is currently underway at the I.E.I.
Mazzanti F, Marzullo C
Being absolutely certain that a program execution will not result in unpredictable behaviour is very difficult. Although there is no way to avoid the underlying theoretical difficulties, we believe that a human-centered approach in exploiting advanced static analysis techniques is a viable solution. This paper presents some preliminary results of a feasibility study on this subject, which is currently underway at the I.E.I.