2006
Software
Unknown
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 ExploRA
2006
Software
Unknown
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 ExploRA
2006
Software
Unknown
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 ExploRA
2007
Software
Unknown
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
See at: CNR ExploRA
2008
Software
Unknown
See at: CNR ExploRA
2003
Report
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.Source: ISTI Technical reports, 2003
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.Source: ISTI Technical reports, 2003
See at:
ISTI Repository 
| CNR ExploRA
2006
Report
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.Source: ISTI Technical reports, 2006
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.Source: ISTI Technical reports, 2006
See at:
ISTI Repository | CNR ExploRA
2006
Report
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.Source: Project report, SENSORIA, Deliverable D3.3.a, 2006
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.Source: Project report, SENSORIA, Deliverable D3.3.a, 2006
See at:
ISTI Repository | CNR ExploRA
2009
Report
Open Access
Designing UML models with UMC
Mazzanti F.
Guida al disegno di modelli UML per il tools UMC v3.6Source: ISTI Technical reports, 2009
Mazzanti F.
Guida al disegno di modelli UML per il tools UMC v3.6Source: ISTI Technical reports, 2009
See at:
ISTI Repository | CNR ExploRA
2011
Contribution to book
Open Access
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.Source: Rigorous Software Engineering for Service-Oriented Systems. Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing, edited by Martin Wirsing, Matthias Hölzl, pp. 408–427. Berlin/Heidelberg: Springer-Verlag, 2011
DOI: 10.1007/978-3-642-20401-2_19
Project(s): SENSORIA
Metrics:
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.Source: Rigorous Software Engineering for Service-Oriented Systems. Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing, edited by Martin Wirsing, Matthias Hölzl, pp. 408–427. Berlin/Heidelberg: Springer-Verlag, 2011
DOI: 10.1007/978-3-642-20401-2_19
Project(s): SENSORIA
Metrics:
See at:
eprints.imtlucca.it | doi.org 
| Archivio istituzionale della ricerca - Alma Mater Studiorum Università di Bologna | link.springer.com | CNR ExploRA
1997
Report
Unknown
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 summarisedSource: ISTI Technical reports, 1997
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 summarisedSource: ISTI Technical reports, 1997
See at: CNR ExploRA
1994
Report
Unknown
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.Source: ISTI Technical reports, pp.i–ii, 1994
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.Source: ISTI Technical reports, pp.i–ii, 1994
See at: CNR ExploRA
1996
Other
Unknown
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.
See at: CNR ExploRA
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.Source: Proceedings of 2nd IEEE International Software Engineering Symposium, Toronto, 1995
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.Source: Proceedings of 2nd IEEE International Software Engineering Symposium, Toronto, 1995
See at:
www.scopus.com | CNR ExploRA
1996
Conference article
Unknown
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.Source: 9th International Software Quality Week, pp. 1–15, San Francisco, USA, 1996
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.Source: 9th International Software Quality Week, pp. 1–15, San Francisco, USA, 1996
See at: CNR ExploRA
1989
Other
Unknown
The point on Ada erroneous executions
Mazzanti F.
Almost all programming languages allow the possibility of an unrecoverable program crashes at run-time. This happens also in the case of Ada. A wider consideration of safety issues during the language maintenance process and in the development of the language implementations would allow to improve the current level of program reliability without any drastic restriction of the language features.
Mazzanti F.
Almost all programming languages allow the possibility of an unrecoverable program crashes at run-time. This happens also in the case of Ada. A wider consideration of safety issues during the language maintenance process and in the development of the language implementations would allow to improve the current level of program reliability without any drastic restriction of the language features.
See at: CNR ExploRA
1989
Contribution to conference
Unknown
Reducing unpredictability in Ada executions
Mazzanti F.
No abstract availableSource: Ada 9x Requirements Workshop, Destin, Florida (USA), May 1989
Mazzanti F.
No abstract availableSource: Ada 9x Requirements Workshop, Destin, Florida (USA), May 1989
See at: CNR ExploRA
1989
Journal article
Unknown
The AIDA experiment
Mazzanti F.
Most of currently available debugging too1s for Ada do not allow to monitor enough in detail the powerful features of the language. For example, the help usually provided to the user for checking the program dependence from the particular characteristics of the language implementation, rarely goes beyond the detection of the most evident aspects. Similarly, no facilities are usually provided for detecting at run-time the occurrence of an erroneous execution, or for driving the program execution in all its aspects to generate the desired program effects. Possible directions for the improvement of debugging techniques to match the needs of Ada, and, more in general, of highly nondeterministic and concurrent languages, have been investigated as part of the activity of the EEC MAP project 755 "SFD-APSE", leading to the development of a prototype of an Advanced Interpreter/Debugger for Ada (AIDA). In this paper the experience gained with the project is briefly summarized, illustrating some of the useful features for a powerful and detailed monitoring of the execution of Ada programs.Source: Ada letters (1981) 9 (1989): 109–114.
Mazzanti F.
Most of currently available debugging too1s for Ada do not allow to monitor enough in detail the powerful features of the language. For example, the help usually provided to the user for checking the program dependence from the particular characteristics of the language implementation, rarely goes beyond the detection of the most evident aspects. Similarly, no facilities are usually provided for detecting at run-time the occurrence of an erroneous execution, or for driving the program execution in all its aspects to generate the desired program effects. Possible directions for the improvement of debugging techniques to match the needs of Ada, and, more in general, of highly nondeterministic and concurrent languages, have been investigated as part of the activity of the EEC MAP project 755 "SFD-APSE", leading to the development of a prototype of an Advanced Interpreter/Debugger for Ada (AIDA). In this paper the experience gained with the project is briefly summarized, illustrating some of the useful features for a powerful and detailed monitoring of the execution of Ada programs.Source: Ada letters (1981) 9 (1989): 109–114.
See at: CNR ExploRA