Dott. Franco Mazzanti

Some Publications

Experimenting with Formal Verification and Model-based Development in Railways: the case of UMC and Sparx Enterprise Architect

Formal Methods for Industrial Critical Systems (FMICS) 2023

Abstract:

The use of formal methods can reduce the time and costs associated with railway signalling systems development and maintenance, and improve correct behaviour and safety. The integration of formal methods into industrial model-based development tools has been the subject of recent research, indicating the potential transfer of academic techniques to enhance industrial tools. This paper explores the integration of an academic formal verification tool, UML Model Checker (UMC), with an industrial model-based development tool, Sparx Enterprise Architect (Sparx EA). The case study being analyzed is a railway standard interface. The paper demonstrates how formal verification techniques from academic tools can be integrated into industrial development practices using industrial tools, and how simulation in Sparx EA can be derived from traces generated by the UMC formal verification activity. From this experience, we derive a set of lessons learned and research challenges.

A Case Study in Formal Analysis of System Requirements

Software Engineering and Formal Methods. SEFM Collocated Workshops, 2023

Abstract:

One of the goals of the 4SECURail project has been to demonstrate the benefits, the limits, and the costs of the introduction of formal methods in the process of definition of system requirements. This has been done, on an experimental basis, by applying a specific set of tools and methodologies to a specific case study from the railway sec- tor. The paper describes the approach adopted in the project, and some considerations resulting from the experience.

Formal Modeling and Initial Analysis of the 4SECURail Case Study

In Models for Formal Analysis of Real Systems (MARS 2022), EPTCS Vol 355, p 118-144, 2022

Abstract:

We present the case study developed in the context of the 4SECURail project and the approach used for its formal modeling and analysis. Starting from a simple SysML/UML behavioral model of the system requirements, three formal models have been developed using three different frameworks, namely UMC, ProB, and CADP/LNT. The paper shows how the different ways to represent and analyze the system from the three different points of view allow us to take advantage of the resulting diversity.

The 4SECURail Formal Methods Demonstrator

RSSRAIL 2022 Springer

Abstract:

The need for high-quality standard interfaces is widely rec- ognized as a mandatory step to reduce procurement costs and create safely operating complex railway infrastructures. That is why European initiatives like EULYNX have been set up precisely with the purpose of supporting standard interfaces development. The exploitation of formal methods during the phase of standardization plays an essential role in raising the quality of the generated specifications. 4SECURail is a recent project that aims to precisely show, with a structured evaluation (known as the formal methods demonstrator), how formal methods might help to improve the quality of a specific signalling interface selected as case study. This paper describes the experience gained with the experiment.

Efficient static analysis and verification of featured transition systems

Empirical software engineering, 2022 Kluwer - Dordrecht

Abstract:

A Featured Transition System (FTS) models the behaviour of all products of a Software Product Line (SPL) in a single compact structure, by associating action-labelled transitions with features that condition their presence in product behaviour. It may however be the case that the resulting featured transitions of an FTS cannot be executed in any product (so called dead transitions) or, on the contrary, can be executed in all products (so called false optional transitions). Moreover, an FTS may contain states from which a transition can be executed only in some products (so called hidden deadlock states). It is useful to detect such ambiguities and signal them to the modeller, because dead transitions indicate an anomaly in the FTS that must be corrected, false optional transitions indicate a redundancy that may be removed, and hidden deadlocks should be made explicit in the FTS to improve the understanding of the model and to enable efficient verification - if the deadlocks in the products should not be remedied in the first place. We provide an algorithm to analyse an FTS for ambiguities and a means to transform an ambiguous FTS into an unambiguous one. The scope is twofold: an ambiguous model is typically undesired as it gives an unclear idea of the SPL and, moreover, an unambiguous FTS can efficiently be model checked. We empirically show the suitability of the algorithm by applying it to a number of benchmark SPL examples from the literature, and we show how this facilitates a kind of family-based model checking of a wide range of properties on FTSs.

4SECURail - Formal development demonstrator prototype, final release

Deliverable 2.5 of the 4SECURail project, 2021,

Abstract:

This final Deliverable of the 4SECURAIL project describes the observed impact of the selected formal methods tools and methodologies for improving the quality of the system requirements specifications.

Compositional Verification of Concurrent Systems by Combining Bisimulations

Formal methods in system design, 2021, Kluwer - Dordrecht

Abstract:

One approach to verify a property expressed as a modal mu-calculus formula on a system with several concurrent processes is to build the underlying state space compositionally (i.e., by minimizing and recomposing the state spaces of individual processes in a hierarchical way, keeping visible only the relevant actions occurring in the formula), and check the formula on the resulting state space. It was shown previously that, when checking the formulas of the Ldbr fragment? of the mu-calculus (consisting of weak modalities only), individual processes can be minimized modulo divergence-preserving branching (divbranching for short) bisimulation. In this paper, we refine this approach to handle formulas containing both strong and weak modalities, so as to enable a combined use of strong or div-branching bisimulation minimization on concurrent processes depending whether they contain or not the actions occurring in the strong modalities of the formula. We extend Ldbr with strong modalities and show that the combined minimization approach preserves the truth value of formulas of the extended fragment. We implemented this approach on top of the CADP verification toolbox and demonstrated how it improves the capabilities of compositional verification on realistic examples of concurrent systems. In particular, we applied our approach to the verification problems of the RERS 2019 challenge and observed drastic reductions of the state space compared to the approach in which only strong bisimulation minimization is used, on formulas not preserved by divbranching bisimulation.

Systematic evaluation and usability analysis of formal methods tools for railway signaling system design

IEEE transactions on software engineering, 2021 IEEE

Abstract:

Formal methods and supporting tools have a long record of success in the development of safety-critical systems. However, no single tool has emerged as the dominant solution for system design. Each tool differs from the others in terms of the modeling language used, its verification capabilities and other complementary features, and each development context has peculiar needs that require different tools. This is particularly problematic for the railway industry, in which formal methods are highly recommended by the norms, but no actual guidance is provided for the selection of tools. To guide companies in the selection of the most appropriate formal methods tools to adopt in their contexts, a clear assessment of the features of the currently available tools is required. To address this goal, this paper considers a set of 13 formal methods tools that have been used for the early design of railway systems, and it presents a systematic evaluation of such tools and a preliminary usability analysis of a subset of 7 tools, involving railway practitioners. The results are discussed considering the most desired aspects by industry and earlier related studies. While the focus is on the railway signaling domain, the overall methodology can be applied to similar contexts. Our study thus contributes with a systematic evaluation of formal methods tools and it shows that despite the poor graphical interfaces, usability and maturity of the tools are not major problems, as claimed by contributions from the literature. Instead, support for process integration is the most relevant obstacle for the adoption of most of the tools. Our contribution can be useful to R&D engineers from railway signaling companies and infrastructure managers, but also to tool developers and academic researchers alike.

Comparing formal tools for system design: a judgment study

ICSE'20 - 42nd International Conference on Software Engineering, 2020, ACM Press ACM Press

Abstract:

Formal methods and tools have a long history of successful applications in the design of safety-critical railway products. However, most of the experiences focused on the application of a single method at once, and little work has been performed to compare the applicability of the different available frameworks to the railway context. As a result, companies willing to introduce formal methods in their development process have little guidance on the selection of tools that couldfi t their needs. To address this goal, this paper presents a comparison between 9 different formal tools, namely Atelier B, CADP, FDR4, NuSMV, ProB, Simulink, SPIN, UMC, and UPPAAL SMC. We performed a judgment study, involving 17 experts with experience in formal methods applied to railways. In the study, part of the experts were required to model a railway signaling problem (a moving-block train distancing system) with the different tools, and to provide feedback on their experience. The information produced was then synthesized, and the results were validated by the remaining experts. Based on the outcome of this process, we provide a synthesis that describes when to use a certain tool, and what are the problems that may be faced by modelers. Our experience shows that the different tools serve different purposes, and multiple formal methods are required to fully cover the needs of the railway system design process.

States and Events in KandISTI: A Retrospective

In: "Models, Mindsets, Meta: The What, the How, and the Why Not?" LNCS 11200, June 2019 Springer

Abstract:

Early work on automated formal verification produced pioneering model-checking algorithms, in which system computations were modelled either as sequences of distinguished states in which the system evolves or as sequences of events or actions occurring during the system's state transitions. In both cases, automata-like structures generally known as transition systems were exploited to capture all possible computations, but still either state-based or event-based. Many years later, both views were combined in descriptions of computations as the evolution between distinguished states by means of transitions characterised by the occurrence of events, and verification tools were adapted to this more general setting. Meanwhile, the most important drive in improving verification tools concerned the complexity of models, which was attacked by algorithms capable of minimising the information needed for deciding the verification questions. One of the outcomes of this quest was local, on-the-fly model checking. Both of these lines of research, pioneered by Bernhard Steffen, are discussed in this paper in a general retrospective on state-based and event-based models of transition systems and temporal logics, followed by an overview of how this is exploited in the KandISTI model-checking environment.

On the industrial uptake of formal methods in the railway domain: a survey with stakeholders

Proceedings of the 14th International Conference on Integrated Formal Methods (IFM'18), LNCS, Springer

Abstract:

The railway sector has seen a large number of successful applications of formal methods and tools. However, up-to-date, structured information about the industrial usage and needs related to formal tools in railways is limited. As a first step to address this, we present the results of a questionnaire submitted to 44 stakeholders with experience in the application of formal tools in railways. The questionnaire was oriented to gather information about industrial projects, and about the functional and quality features that a formal tool should have to be successfully applied in railways. The results show that the most used tools are, as expected, those of the B family, followed by an extensive list of about 40 tools, each one used by few respondents only, indicating a rich, yet scattered, landscape. The most desired features concern formal verification, maturity, learnability, quality of documentation, and ease of integration in a CENELEC process. This paper extends the body of knowledge on formal methods applications in the railway industry, and contributes with a ranked list of tool features considered relevant by railway stakeholders.

Ten Diverse Formal Models for a CBTC Automatic Train Supervision System

3rd Workshop on Models for Formal Analysis of Real Systems (MARS 2018), 20 October 2018, Thessaloniki, Greece

Abstract:

Communications-based Train Control (CBTC) systems are metro signalling platforms, which coordinate and protect the movements of trains within the tracks of a station, and between different stations. In CBTC platforms, a prominent role is played by the Automatic Train Supervision (ATS) system, which automatically dispatches and routes trains within the metro network. Among the various functions, an ATS needs to avoid deadlock situations, i.e., cases in which a group of trains block each other. In the context of a technology transfer study, we designed an algorithm for deadlock avoidance in train scheduling. In this paper, we present a case study in which the algorithm has been applied. The case study has been encoded using ten different formal verification environments, namely UMC, SPIN, NuSMV/nuXmv, mCRL2, CPN Tools, FDR4, CADP, TLA+, UPPAAL and ProB. Based on our experience, we observe commonalities and differences among the modelling languages considered, and we highlight the impact of the specific characteristics of each language on the presented models.

Towards Formal Methods Diversity in Railways: an Experience Report with Seven Frameworks

International Journal on Software Tools for Technology Transfer, STTT 20(3)

Abstract:

In the ever expanding universe of formal methods, several tools exist that can be exploited to validate early system designs, and that are applicable to problems of the railway domain. In this paper, we present an experience report in formal modelling and verification using seven different formal environments, namely UMC, Promela/SPIN, NuSMV, mCRL2, CPN Tools, FDR4 and CADP. In particular, we model and verify an algorithm that addresses a typical railway problem, namely deadlock avoidance in train scheduling. The algorithm is designed according to a prototypical architecture, the so-called blackboard pattern, in which a set of global data is atomically updated by a set of concurrent guarded agents. Our experience, limited to the specific problem, shows that the design of the algorithm can be translated into the different formalisms with acceptable effort, while deep proficiency with the tools is required to optimise the performance. The current paper establishes the preliminary foundations for the concept of formal methods diversity in the development of railway systems. The concept is based on the idea that, if different non-certified formal environments are used to verify the same design, this increases the confidence on the verification results. Furthermore, by checking that the number of states generated during the verification process is the same for each framework, the designer can have an initial indication of the equivalence of the diverse models. The industrial application of this promising concept requires further research, and appropriate guidelines shall be established to identify the proper formal environments to use for a specific railway problem, and to define an industrial process in which formal methods diversity can be exploited at its full benefits. The paper presents the different models developed, compares the tools employed in terms of language features and performance, and disacusses the industrial implications of the concept of for- mal methods diversity in the railway domain.

Experiments in Formal Modelling of a Deadlock Avoidance Algorithm for a CBTC System

7th International Symposium on leveraging applicationsof formal methods, verification and validation- ISOLA 2016; October 2016 Corfu; Greece

Abstract:

This paper presents a set of experiments in formal modelling and verification of a deadlock avoidance algorithm of an Automatic Train Supervision System (ATS). The algorithm is modelled and verified using four formal environment, namely UMC, Promela/SPIN, NuSMV, and mCRL2. The experience gained in this multiple modelling/verification experiments is described. We show that the algorithm design, structured as a set of concurrent activities cooperating through a shared memory, can be replicated in all the formal frameworks taken into consideration with relative effort. In addition, we highlight specific peculiarities of the various tools and languages, which emerged along our experience.

An experience in Ada multicore programming: Parallelisation of a model checking engine

21st Ada-Europe International Conference on Reliable Software Technologies, Ada-Europe 2016; Lecture Notes in Computer Science Volume 9695, 2016, Pages 94-109

Abstract:

Even if multicore architectures are nowadays extremely wide-spread, the exploitation of this easily available degree of parallelism is not always straightforward. In this paper we describe the experience gained in our ongoing effort to parallelise the model checking engine of a family of model checkers (KandISTI) developed at ISTI. The main focus of our experimentation is the evaluation of the minimal efforts needed to take advantage of our everyday multicore hardware for model checking purposes. Our early results relative to an initial fragment of the logic show a speedup factor of about 2.5 when 4 physical cores are available. This result, however, can only be achieved by complementing the initial high level Ada design with a second round of code fine-tuning which exploits nonstandard low level features in the implementation of the needed thread-safe data structures.

Modelling and Analysing Variability in Product Families: Model Checking of Modal Transition Systems with Variability Constraints

Journal of Logical and Algebraic Methods in Programming. Volume 85, Issue 2, February 2016, Pages 287-315

Abstract:

We present the formal underpinnings of a modelling and analysis framework for the specification and verification of variability in product families. We ad- dress variability at the behavioural level by modelling the family behaviour by means of a Modal Transition System (MTS) with an associated set of variabil- ity constraints expressed over action labels. An MTS is a Labelled Transition System (LTS) which distinguishes between optional and mandatory transitions. Steered by the variability constraints, the inclusion or exclusion of labelled tran- sitions in an LTS refining the MTS determines the family’s possible product behaviour. We formalise this as a special-purpose refinement relation for MTSs, which differs fundamentally from the classical one, and show how to use it for the definition and derivation of valid product behaviour starting from product family behaviour. We also present a variability-aware action-based branching- time modal temporal logic to express properties over MTSs, and demonstrate a number of results regarding the preservation of logical properties from family to product behaviour. These results pave the way for the more efficient family- based analyses of MTSs, limiting the need for product-by-product analyses of LTSs. Finally, we define a high-level modal process algebra for the specification of MTSs. The complete framework is implemented in a model-checking tool: given the behaviour of a product family modelled as an MTS with an additional set of variability constraints, it allows the explicit generation of valid product behaviour as well as the efficient on-the-fly verification of logical properties over family and product behaviour alike.

Using FMC for family-based analysis of software product lines

19th International Software Product Line Conference, SPLC 2015; Nashville; United States; 20 July 2015 through 24 July 2015; ACM International Conference Proceeding Series Volume 20-24-July-2015, 20 July 2015, Pages 432-439

Abstract:

We show how the FMC model checker can successfully be used to model and analyze behavioural variability in Software Product Lines. FMC accepts parameterized specifications in a process-algebraic input language and allows the verification of properties of such models by means of efficient on-the-fly model checking. The properties can be expressed in a logic that allows to correlate the parameters of different actions within the same formula. We show how this feature can be used to tailor formulas to the verification of only a specific subset of products of a Software Product Line, thus allowing for scalable family-based analyses with FMC. We present a proof-of-concept that shows the application of FMC to an illustrative Featured Transition System from the literature.

From EU projects to a family of model checkers

Lecture Notes in Computer Science Volume 8950, 2015, Pages 312-328

Abstract:

We describe the development of the KandISTI family of model checkers from its origins nearly two decades ago until its very recent latest addition. Most progress was made, however, during two integrated European projects, AGILE and SENSORIA, in which our FM&&T lab participated under the scientific coordination of Martin Wirsing. Moreover, the very name of the family of model checkers is partly due to Martin Wirsing’s passion for art and science.

VMC: Recent advances and challenges ahead

18th International Software Product Line Conference, SPLC 2014; Florence; Italy; ACM International Conference Proceeding Series Volume 2, 15 September 2014, Pages 70-77

Abstract:

The variability model checker VMC accepts a product family specified as a Modal Transition System (MTS) with additional variability constraints. Consequently, it offers behavioral variability analyses over both the family and its valid product behavior. This ranges from product derivation and simulation to efficient on-the-fly model checking of logical properties expressed in a variability-aware version of actionbased CTL. In this paper, we first explain the reasons and assumptions underlying the choice for a modeling and analysis framework based on MTSs. Subsequently, we present recent advances on proving inheritance of behavioral analysis properties from a product family to its valid products. Finally, we illustrate challenges remaining for the future.

Designing a deadlock-free train scheduler: A model checking approach

6th NASA Formal Methods Symposium, NFM 2014; Houston, TX; United States; Lecture Notes in Computer Science,Volume 8430, 2014, Pages 264-269

Abstract:

In this paper we present the approach used in the design of the scheduling kernel of an Automatic Train Supervision (ATS) system. A formal model of the railway layout and of the expected service has been used to identify all the possible critical sections of the railway layout in which a deadlock might occur. For each critical section, the prevention of the occurrence of deadlocks is achieved by constraining the set of trains allowed to occupy these sections at the same time. The identification of the critical sections and the verification of the correctness of the logic used by the ATS is carried out by exploiting a model checking verification framework locally developed at ISTI-CNR and based on the tool UMC.

Deadlock avoidance in train scheduling: A model checking approach

19th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2014; Florence; Lecture Notes in Computer Science Volume 8718, 2014, Pages 109-123

Abstract:

In this paper we present the deadlock avoidance approach used in the design of the scheduling kernel of an Automatic Train Supervision (ATS) system. The ATS that we have designed prevents the occurrence of deadlocks by performing a set of runtime checks just before allowing a train to move further. For each train, the set of checks to be performed at each step of progress is retrieved from statically generated ATS configuration data. For the verification of the correctness of the logic used by the ATS and the validation of the constraints verified by the runtime checks, we define a formal model that represents the ATS behavior, the railway layout, and the planned service structure. We use this formal model to verify both the absence of deadlocks and absence of false positives (i.e., cases in which a train is unnecessarily disallowed to proceed). The verification is carried out by exploiting the UMC model checking verification framework locally developed at ISTI-CNR.

A Logical Verification Methodology for Service-Oriented Computing

ACM Transactions on Software Engineering and Methodology, volume 21, number 3, pages 16:01-16:46. ACM Press, 2012.

Abstract:

We introduce a logical verification methodology for checking behavioural properties of service-oriented computing systems. Service properties are described by means of SocL, a branching-time temporal logic that we have specifically designed to express in an effective way distinctive aspects of services, such as, e.g., acceptance of a request, provision of a response, and correlation among service requests and responses. Our approach allows service properties to be expressed in such a way that they can be independent of service domains and specifications. We show an instantiation of our general methodology that uses the formal language COWS to conveniently specify services and the expressly developed software tool CMC to assist the user in the task of verifying SocL formulae over service specifications. We demonstrate feasibility and effectiveness of our methodology by means of the specification and the analysis of a case study in the automotive domain.

An Abstract, on the Fly Framework for the Verification of Service-Oriented Systems

SENSORIA Project - Lecture Notes in Computer Science 6582, pp. 390-407, 2011

Abstract:

In this chapter we present (some of) the design principles which have inspired the development of the CMC/UMC verification framework. The first of these is the need of an abstraction mechanism which allows to observe a model in terms of an abstract L2 T S , therefore hiding all the unnecessary underlying details of the concrete computational model, while revealing only the details which might be important to understand the system behavior. The second of these is the need a Service-Oriented Logic (SocL ) which is an event and state based, branching-time, efficiently verifible, parametric temporal logic, for the formal encoding of service-oriented properties. The third principle is the usefulness of an on-the-fly, bounded model-checking approach for an efficient, interactive analysis of service-oriented systems which starts from the early stages of the incremental system design

"A state/event-based model-checking approach for the analysis of abstract system properties"

Science of Computer Programming 76, 2 (2011), 119 - 135.

Abstract:

We present the UMC framework for the formal analysis of concurrent systems specified by collections of UML state machines. The formal model of a system is given by a doubly labelled transition system, and the logic used to specify its properties is the state-based and event-based logic UCTL. UMC is an on-the-fly analysis framework which allows the user to interactively explore a UML model, to visualize abstract behavioural slices of it and to perform local model checking of UCTL formulae. An automotive scenario from the service- oriented computing (SOC) domain is used as case study to illustrate our approach.

An Experience on Formal Analysis of a high-level graphical SOA Design

Proceedings of the Second International Workshop on Formal Methods and Agile Methods (FM+AM'10), Pisa, Italy (S. Gruner and B. Rumpe, eds.), Lecture Notes in Informatics 179, Gesellschaft für Informatik, Bonn, 2010, 7-98.

Abstract:

In this paper, we present the experience gained with the participation in a case study in which a novel high-level design language (UML4SOA) was used to produce a service-oriented system design, to be model checked with respect to the intended requirements and automatically translated into executable BPEL code. This experience, beyond revealing several uncertainties in the language definition, and several flaws in the designed model, has been useful to better understand the hidden risks of apparently intuitive graphical designs, when these are not backed up by a precise and rigorous semantics. The adoption of a rigorous or formal semantics for these notations, and the adoption of formal verification methods allow the full exploration of designs which otherwise risk to become simple to draw and update, but difficult to really understand in all their hidden ramifications. Automatic formal model generation from high level graphical designs is not only desirable but also pragmatically feasible e.g. using appropriate model transformation techniques. This is particularly valuable in the context of agile development approaches which are based on rapid and continuous updates of the system designs.

A model-checking approach for service component architectures"

Proceedings FMOODS/FORTE 2009 - Formal Techniques for Distributed Systems. Joint 11th IFIP WG 6.1 International Conference FMOODS 2009 and 29th IFIP WG 6.1 International Conference FORTE 2009 (D. Lee, A. Lopes and A. Poetzsch-Heffter, Eds.), LNCS 5522, 2009, 219-224

Abstract:

We present a strategy for model-checking the correctness of service composition. We do so in the context of SRML, a formal modelling framework for service-oriented computing being defined within the SENSORIA project. We introduce a methodology for encoding patterns of typical service interaction with UML state machines and present a strategy for checking SRML specifications of service composition based on such patterns. For that purpose, we use the action-state branching time temporal logic UCTL and the model-checker UMC.

CMC-UMC: A Framework for the Verification of Abstract Service-Oriented Properties

Proceedings of the 24th Annual ACM Symposium on Applied Computing (SAC'09), Honolulu, Hawaii, USA, ACM Press, 2009, 1844 - 1850

Abstract:

CMC and UMC are two prototypical instantiations of a common logical verification framework for the analysis of functional properties of service-oriented systems. The service oriented SocL logic is used to describe the required system properties. Computational models of the system can be built either using the COWS speci cation language or designing the system as a collection of interacting UML state machines, and an on-the-fly model checker can be used to verify the satisfaction of the requirements and possibly to generate counterexamples or witnesses for them. An automotive case study is used to illustrate the overall framework.

A model checking approach for verifying COWS specifications

Proc. of Fundamental Approaches to Software Engineering (FASE'08). J. L. Fiadeiro, P. Inverardi (Eds.). pp. 230-245. LNCS vol. 4961. Springer. 2008

Abstract:

We introduce a logical verification framework for checking functional properties of service-oriented applications formally specified using the service specification language COWS. The properties are described by means of a service-oriented logic, called SocL, that is a specialization of the logic UCTL to capture peculiar aspects of services. Service behaviours are abstracted in terms of Doubly Labelled Transition Systems that describe all their possible evolutions and are used as the interpretation domain for SocL formulae. We also illustrate the SocL model checker at work on a bank service scenario specified in COWS.

"Formal Verification of an Automotive Scenario in Service-Oriented Computing"

In Proceedings of the 30th International Conference on Software Engineering (ICSE'08), Leipzig, Germany. pp. 613-622. ACM Press. 2008.

Abstract:

We report on the successful application of academic experience with formal modelling and verification techniques to an automotive scenario from the field of service-oriented computing. The aim of this industrial case study is to verify a priori , thus before implementation, certain design issues. The specific scenario is one of the outcomes of discussions with automotive experts on possible new services for drivers to be provided by the in-vehicle computers.

"An action/state-based model-checking approach for the analysis of communication protocols for Service-Oriented Applications"

In Proceedings of the 12th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'07), Berlin, Germany, Lecture Notes in Computer Science, Springer-Verlag, Berlin, 2007.

Abstract:

In this paper we present an action/state-based logical framework for the analysis and verification of complex systems, which relies on the definition of doubly labelled transition systems. The defined temporal logic, called UCTL, combines the action paradigm - classically used to describe systems using labelled transition systems - with predicates that are true over states - as captured when using Kripke structures - as semantic model. An efficient model checker for UCTL has been realized, exploiting an on-the-fly algorithm. We then show how to use UCTL, and its model checker, in the design phase of an asynchronous extension of the communication protocol SOAP, called aSOAP. For this purpose, we describe aSOAP as a set of communicating UML state machines, for which a semantics over doubly labelled transition systems has been provided.

"Formal Modelling and Verification of an Asynchronous Extension of SOAP"

In Proceedings of the 4th IEEE European Conference on Web Services (ECOWS'07), Zurich, Switzerland (A. Bernstein, T. Gschwind, and W. Zimmermann, eds.), IEEE Computer Society, Los Alamitos, CA, 2006, 287 - 296.

Abstract:

Current web services are largely based on a synchronous request-response model that uses the Simple Object Access Protocol SOAP. Next-generation telecommunication networks, on the contrary, are characterised by the need to handle asynchronous interactions among distributed service components, e.g., to deal with long-running computations and with events produced by the network resources. As these worlds are more and more converging into a single application context, several solutions have been proposed to deal with asynchronous events in the context of web services. In this paper we formalise and verify one such approach, viz., an original asynchronous extension of SOAP, and draw some conclusions. The formal model is specified as a set of communicating state machines. The semantics of the model is seen as a doubly-labelled transition system, and its behavioural properties are expressed in the actionand state-based temporal logic mu-UCTL and verified with the on-the-fly model checker UMC.

"UMC 3.3 User Guide"

ISTI Technical Report 2006-TR-33 , September 2006

Abstract:

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 command-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.

"A Model Checking Verification Environment for UML Statecharts"

XLIII Congresso Annuale AICA, Udine 5-7 Ottobre 2005

Abstract:

In this paper we present the state/event-based temporal logic mu-UCTL which is a logic oriented towards a natural description of dynamic properties of UML models. This logic allows to specify the basic properties that a runtime system configuration should satisfy and to combine these basic predicates with logic and temporal operators which allow to take into consideration also the events performed by the system when evolving from one system configuration to another. Doubly Labelled Transition Systems are the semantic domain for mu-UCTL. The logic is supported by a prototypical verification environment under development at ISTI built around the "on the fly" UMC model checker.

"On the fly model checking of communicating UML State Machines"

Second ACIS International Conference on Software Engineering Research Management and Applications (SERA2004) (Los Angeles, USA, 5-7 May 2004).

Abstract:

In this paper we present an 'on the fly' model checker for the verification of the dynamic behavior of UML models seen as a set of communicating state machines. The logic supported by the tool is an extension of the action based branching time temporal logic mu-ACTL and has the power of full mu-calculus. Early results on the application of this model checker to a case study have been also reported.

"AGILE: Software Architectures for Mobility"

in Recent Trends in Algebraic Development, LNCS 2755 , Springer Verlag, November 2003

Abstract:

Architecture-based approaches have been promoted as a means of controlling the complexity of system construction and evolution, in particular for providing systems with the agility required to operate in turbulent environments and to adapt very quickly to changes in the enterprise world. recent technological advances in communication and distribution have made mobility an additional factor of complexity, one for which current architectural concepts and techniques can be hardly used. The AGILE project is developing an architectural approach in which mobility aspects can be modelled explicitly and mapped on the distribution and communication topology made available at physical levels. The whole approach is developed over a uniform mathematical framework based on graph-oriented techniques that support sound methodological priciples, formal analysis, and refinement. The paper describes the AGILE project and some of the results gained duriong the first project year.

"UMC User Guide (Version 2.5)"

ISTI Technical Report 2003-TR-22 , September 2003

Abstract:

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.

"On the Fly Verification of Networks of Automata"

International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99), special session on Current limits to automated verification for distributed systems, CSREA, 1999.

Abstract:

In this paper we present an "on the fly model checker" for the action based branching time temporal login mu-ACTL. The model checker allows a logic formula to be evaluated directly on the network representing a concurrent system as a collection of synchronized agents working in parallel, without generating the global model of the system. It is possible in this way to verify interesting properties also on systems for which the state explosion problem makes other verification tools inapplicable.

"Deductive proof of Software Properties"

Ercim News, N.36, January 1999, p.15-16.

Abstract:

The aim of an recently begun IEI project is to experiment with the idea that a deductive approach can successfully be adopted to support the verification of properties of programs written in high level languages.

"A Symbolic Model Checker for Action-based CTL"

Proceeding International Workshop on Current Trends in Applied Formal Methods (FM-Trends 98), Boppard, Germany, 7-9 October 1998 also LNCS 1641, Springer - Verlag, 1999

Abstract:

We present SAM, a symbolic model checker for ACTL, the action-based version of CTL. SAM relies on implicit representations of Labeled Transition Systems (LTSs), the semantic domain for ACTL formulae, and makes use of symbolic manipulation algorithms. SAM has been realized by translating (networks of) LTSs and, possibly recursive, ACTL formulae into BSP (Boolean Symbolic Programming), a programming language aiming at defining computations on boolean functions, and by using the BSP interpreter to carry out computations (i.e. verifications).

"Formalising Engineering Judgement on Software Dependability via Belief Networks"

Proceedings of Sixth IFIP International Working Conference on Dependable Computing for Critical Applications. Garmisch-Partenkirchen, Germany, 1997

Abstract:

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.

"Guide to Erroneous Executions in Ada 95"

I.E.I. Technical Report B4-20 1997

Abstract:

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.

"Towards the static detection of erroneous executions in Ada 95"

Ninth International Software Quality Week '96 (QW'96)
Sheraton Palace Hotel, San Francisco, California USA, 21-24 May 1996

Abstract:

Acquiring complete confidence that a program execution will not result in an unpredictable behaviour is very difficult. Even if the theoretical difficulties cannot be eliminated, a human centred approach in exploiting advanced static analysis techniques is claimed to be viable solution. The preliminary results of a feasibility study being carried on at I.E.I. are presented.

"Coding Regulations for Safety Critical Software Development"

Proceedings Second International Software Engineering Symposium, ISSES'95,
Toronto, Aug 1995

Abstract:

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.

"Experimenting dynamic linking with Ada"

Software Practice and Experience,
vol.23, n.1, January 1993, pp. 1-14.

Abstract:

An approach to achieving dynamic reconfiguration within the framework of the Ada programming language is described. A technique for introducing a kernel facility for dynamic reconfiguration in Ada is illustrated and its implementation, using the Verdix VADS 5.5 Ada compiling system on a SUN3-120 running the BSD Unix version 4.3 operating system is discussed. This experimental kernel allows an Ada program to dynamically change its own configuration, linking new pieces of code at run-time. It is shown how this dynamic facility can be consistently integrated at the Ada language level, without introducing severe inconsistencies with respect to the Standard semantics.

"Reducing the risk of destructive errors"

In "Ada in Aerospace",
Proceedings of Second Symposium EUROSPACE, January 1992.

Abstract:

Ada, similarly to most other programming languages, does not prevent the possibility of destructive errors, i.e. errors which are likely to corrupt the program execution status or to kill the program itself. An overview of this kind of errors is given, and the way to avoid them by adopting a safe programming style is outlined. The current Ada9X approach for reducing this risk in the next version of the language is presented.

"The risk of destructive run-time errors"

ACM Ada Letters Vol XI no 1 January/February 1991

Abstract:

We introduce the class of destructive run-time errors as those errors after which the execution status of the program can be so damaged that it is usually impossible to perform any kind of program-driven recovery. Programming errors causing this destructive events are analysed, with particular attention to those cases not related to the use of explicitly "dangerous" low level constructs. It is shown how the risk of these errors can be easily underestimated.

"A Survey of the Implementation Dependent Aspects of Ada",

Journal of Pascal, Ada & Modula2, JohnJWiley &Sons, Vol.8 no.4 Jul/Aug 1989

Abstract:

Although Ada is an ANSI standard, the portability aspects, the predictability of the effects, and the semantic definition of programs using some of the features which are "on the border" of the language are very complex and confused. The aim of this work is to clarify the effects on the portability of programs and the meaning of the use of the features of Ada which appear to be "implementation-dependent". In particular, the different types of implementation dependencies which are allowed by the current definition of Ada are illustrated providing a classification based on the qualitative differences among them, and other aspects which might incorrectly be considered implementation dependencies (e.g. incorrect order dependencies and some nondeterministic aspects) are pointed out.

"The Ada Challenge for new Formal Semantic Techniques"

In "Ada: Managing the Transition", Proceedings 1986 Ada-Europe Conference,
The Ada Companion Series, Cambridge University Press, May 1986.

Abstract:

Ada is posing new challenging problems in the field of formal definitions, as it is witnessed by the many attempts at a solution. We argue that the CEC-MAP project on AdaFD could be considered a new startinbg point, meeting the challenge to some extent. Indeed, following the SMoLCS methodology, the dynamic sematics is split in two parts, formalizing a model for the undelying concurrent structure and then connecting the abstract syntax to that model by a set denotational, hence compositional, clauses. The formal model is given as an abstract data type which accomodates an operational semantics of concurrency and a parameterized modular specification of all needed structures. We outline how the followed approach can handle some of the basic problems, particularly the interference between sequential and concurrent features, togethr with permitting a local correspondence with the Language Reference Manual. We also point out some problems still to be settled.