2005
Journal article
Restricted
A comparison between handwritten and automatic generation of C code from SDL using static analysis
Becucci M, Fantechi A, Giromini M, Spinicci E
The experience reported in this paper relates to an evaluation of the automatic generation of C code from the Specification and Description Language (SDL) specification of embedded applications. The evaluation has been carried out by comparing the automatically generated code with the manually implemented code, both compliant to the same SDL specification: this comparison is based on a selection of metrics measured on both codes by means of commercial static analysis tools. Notwithstanding the different structure of the two codes, we appropriately selected and aggregated the obtained results in order to use them as indicators of code size, control flow complexity and integration flow complexity. For a better comparison of the two codes, we have also introduced a novel complexity metric, which compares the control flow complexity with the integration flow of the two different software architectures. The aim of the paper is not merely to evaluate the code generator used, but rather to propose a set of techniques that can be used to conduct similar evaluations.Source: SOFTWARE, PRACTICE AND EXPERIENCE, vol. 35 (issue 14), pp. 1317-1347
DOI: 10.1002/spe.673
Metrics:
Becucci M, Fantechi A, Giromini M, Spinicci E
The experience reported in this paper relates to an evaluation of the automatic generation of C code from the Specification and Description Language (SDL) specification of embedded applications. The evaluation has been carried out by comparing the automatically generated code with the manually implemented code, both compliant to the same SDL specification: this comparison is based on a selection of metrics measured on both codes by means of commercial static analysis tools. Notwithstanding the different structure of the two codes, we appropriately selected and aggregated the obtained results in order to use them as indicators of code size, control flow complexity and integration flow complexity. For a better comparison of the two codes, we have also introduced a novel complexity metric, which compares the control flow complexity with the integration flow of the two different software architectures. The aim of the paper is not merely to evaluate the code generator used, but rather to propose a set of techniques that can be used to conduct similar evaluations.Source: SOFTWARE, PRACTICE AND EXPERIENCE, vol. 35 (issue 14), pp. 1317-1347
DOI: 10.1002/spe.673
Metrics:
See at:
Software Practice and Experience 
| CNR IRIS | CNR IRIS | onlinelibrary.wiley.com
2006
Journal article
Restricted
A story about formal methods adoption by a railway signaling Manufacturer
Bacherini S, Fantechi A, Tempestini M, Zingoni N
This paper reports the story of the introduction of formal methods in the development process of a railway signaling manufacturer. The first difficulty for a company is due to the many different formal methods proposals around; we show how this difficulty has been addressed and how the choice of a reference formal specification notation and of the related tools has been driven by many external factors related to the specific application domain, to the company policies, to european regulations. Cooperation with University has been fundamental in this process, which is now at the stage in which internal acceptance of the chosen formalisms and tools is established
Bacherini S, Fantechi A, Tempestini M, Zingoni N
This paper reports the story of the introduction of formal methods in the development process of a railway signaling manufacturer. The first difficulty for a company is due to the many different formal methods proposals around; we show how this difficulty has been addressed and how the choice of a reference formal specification notation and of the related tools has been driven by many external factors related to the specific application domain, to the company policies, to european regulations. Cooperation with University has been fundamental in this process, which is now at the stage in which internal acceptance of the chosen formalisms and tools is established
See at:
CNR IRIS | CNR IRIS | www.springerlink.com
2008
Conference article
Open Access
Session types for orchestration charts
Fantechi A, Najm E
We present a novel approach for the sound orchestration of services. It is based on Orcharts and Typecharts: a service orchestra- tion language and an associated behavioural typing language. Sessions play a pivotal role in this approach. Orcharts (orchestration charts) de- fine session based services and Typecharts provide for session types with complex interaction patterns that generalise the request/response inter- action paradigm. We provide an algorithm for deciding behavioural well typedeness. We claim that well typed service configurations have the soudness property, i.e., any session that can be initiated in a well typed configuration has its requestor and provider behave in mutual confor- mance and potentially reach service completion.DOI: 10.1007/978-3-540-68265-3_8
Metrics:
Fantechi A, Najm E
We present a novel approach for the sound orchestration of services. It is based on Orcharts and Typecharts: a service orchestra- tion language and an associated behavioural typing language. Sessions play a pivotal role in this approach. Orcharts (orchestration charts) de- fine session based services and Typecharts provide for session types with complex interaction patterns that generalise the request/response inter- action paradigm. We provide an algorithm for deciding behavioural well typedeness. We claim that well typed service configurations have the soudness property, i.e., any session that can be initiated in a well typed configuration has its requestor and provider behave in mutual confor- mance and potentially reach service completion.DOI: 10.1007/978-3-540-68265-3_8
Metrics:
See at:
Flore (Florence Research Repository) 
| doi.org | CNR IRIS | CNR IRIS | link.springer.com
2009
Book
Open Access
Preface to FMICS 2008
Cofer D, Fantechi A
The aim of the FMICS workshop series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. In particular, these workshops are intended to bring together scientists and practitioners who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. These workshops also strive to promote research and development for the improvement of formal methods and tools for industrial applications.DOI: 10.1007/978-3-642-03240-0
Metrics:
Cofer D, Fantechi A
The aim of the FMICS workshop series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. In particular, these workshops are intended to bring together scientists and practitioners who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. These workshops also strive to promote research and development for the improvement of formal methods and tools for industrial applications.DOI: 10.1007/978-3-642-03240-0
Metrics:
See at:
CNR IRIS | link.springer.com | doi.org | CNR IRIS
2005
Journal article
Restricted
Assembling components with behavioural contracts = Assemblage de composants selon des contrats comportementaux
Carrez C, Fantechi A, Najm E
Component based design is a new paradigm to build distributed systems and applications. The problem of compositional verification of such systems is however still open. We investigate methods and concepts for the provision of 'sound' assemblies. We define a behavioural interface type language endowed with a (decidable) set of interface compatibilty and subtyping rules. We define an abstract, dynamic, multi-threaded, component model, encompassing both client/server and peer to peer communication patterns. Based on the notion of compliance of components to their interfaces, we define the concepts of 'contract' and 'contract satisfaction'. This leads to sound assemblies of components, which possess interesting properties, such as 'external deadlockfreeness' and 'message consumption'.Source: ANNALES DES TÉLÉCOMMUNICATIONS, vol. 60 (issue 7-8), pp. 989-1022
Carrez C, Fantechi A, Najm E
Component based design is a new paradigm to build distributed systems and applications. The problem of compositional verification of such systems is however still open. We investigate methods and concepts for the provision of 'sound' assemblies. We define a behavioural interface type language endowed with a (decidable) set of interface compatibilty and subtyping rules. We define an abstract, dynamic, multi-threaded, component model, encompassing both client/server and peer to peer communication patterns. Based on the notion of compliance of components to their interfaces, we define the concepts of 'contract' and 'contract satisfaction'. This leads to sound assemblies of components, which possess interesting properties, such as 'external deadlockfreeness' and 'message consumption'.Source: ANNALES DES TÉLÉCOMMUNICATIONS, vol. 60 (issue 7-8), pp. 989-1022
2005
Conference article
Restricted
Geographical vs. Functional modelling by statecharts of interlocking systems
Banci M, Fantechi A
The development of computer controlled Railway Interlocking Systems (RIS) has seen an increasing interest in the use of Formal Methods, due to their ability to precisely specify the logical rules that guarantee the safe establishment of routes for trains through a railway yard. Recently, a trend has emerged about the use of statecharts as a standard formalism to produce precise specifications of RIS. This paper describes an experience in modelling a railway interlocking system using statecharts. Our study has addressed the problem from a 'geographical', distributed, point of view: that is, our model is composed by models of single physical entities (points, signals, etc..) that collectively implement the interlocking rules, without any centralized database of rules, which is on the other hand a typical way of implementing such a system (what we call 'functional' approach). One of the main aims of our approach, is to verify its ability to reduce revalidation efforts in the case of physical modifications to the yard; we show how the geographical approach may reduce this effort by requiring only the revalidation of those software modules that are actually affected by the changes.
Banci M, Fantechi A
The development of computer controlled Railway Interlocking Systems (RIS) has seen an increasing interest in the use of Formal Methods, due to their ability to precisely specify the logical rules that guarantee the safe establishment of routes for trains through a railway yard. Recently, a trend has emerged about the use of statecharts as a standard formalism to produce precise specifications of RIS. This paper describes an experience in modelling a railway interlocking system using statecharts. Our study has addressed the problem from a 'geographical', distributed, point of view: that is, our model is composed by models of single physical entities (points, signals, etc..) that collectively implement the interlocking rules, without any centralized database of rules, which is on the other hand a typical way of implementing such a system (what we call 'functional' approach). One of the main aims of our approach, is to verify its ability to reduce revalidation efforts in the case of physical modifications to the yard; we show how the geographical approach may reduce this effort by requiring only the revalidation of those software modules that are actually affected by the changes.
2005
Conference article
Restricted
Instantiating generic charts for railway interlocking systems
Banci M, Fantechi A
The development of computer controlled Railway Interlocking Systems has seen an increasing interest in the use of Formal Methods, due to their ability to precisely specify the logical rules that guarantee the safe establishment of routes for trains through a railway yard. Recently, a trend has emerged about the use of statecharts as a standard formalism to produce precise specifications of these systems. A problem that arises in the practical application of such formalization is that each produced interlocking system is dependent on the physical layout of the controlled yard. This has strong effects on development costs and especially on validation, which has to be repeated for each product. Validating formalized interlocking principles first, and then instantiating them to a specification which is tailored to the considered layout is a solution that we investigate in this paper.
Banci M, Fantechi A
The development of computer controlled Railway Interlocking Systems has seen an increasing interest in the use of Formal Methods, due to their ability to precisely specify the logical rules that guarantee the safe establishment of routes for trains through a railway yard. Recently, a trend has emerged about the use of statecharts as a standard formalism to produce precise specifications of these systems. A problem that arises in the practical application of such formalization is that each produced interlocking system is dependent on the physical layout of the controlled yard. This has strong effects on development costs and especially on validation, which has to be repeated for each product. Validating formalized interlocking principles first, and then instantiating them to a specification which is tailored to the considered layout is a solution that we investigate in this paper.
2005
Conference article
Open Access
Validation coverage for a component-based SDL model of a railway signaling system
Banci M, Becucci M, Fantechi A, Spinicci E
In this paper we present an application of formal verification techniques to a component-based SDL model of a railway signalling system lent by General Electric Transportation Systems. A MSC-driven validation technique has been applied to verify the multiple-configuration features of the system. This work addresses the problem of validating a component-oriented designed SDL model, with a partial reuse of previously verified MSC scenarios if a new component is introducing or modified: some possible solutions based on the coverage metrics and information provided by the adopted tools are discussed.DOI: 10.1016/j.entcs.2004.02.083
Metrics:
Banci M, Becucci M, Fantechi A, Spinicci E
In this paper we present an application of formal verification techniques to a component-based SDL model of a railway signalling system lent by General Electric Transportation Systems. A MSC-driven validation technique has been applied to verify the multiple-configuration features of the system. This work addresses the problem of validating a component-oriented designed SDL model, with a partial reuse of previously verified MSC scenarios if a new component is introducing or modified: some possible solutions based on the coverage metrics and information provided by the adopted tools are discussed.DOI: 10.1016/j.entcs.2004.02.083
Metrics:
See at:
Electronic Notes in Theoretical Computer Science | CNR IRIS | CNR IRIS
2009
Book
Metadata Only Access
Informatica industriale
Fantechi A
Embedded systems are becoming more and more pervasive in daily life. Standard hardware/software design techniques can be a sufficient background for the realization of such systems, but the actual design of embedded systems displays multiple critical aspects that deserve to be addressed. Together with the specific techniques for the design of such systems (processors characteristics, real time aspects, etc.), this book introduces concepts such as reliability, availability, safety, and describes the techniques adopted to associate these attributes to a system, with constant reference to the current norms and regulations belonging to various application domains. This book comes from the more than ten years research/teaching experience of the author on these topics, not only in academia, but also in several industrial settings. It is therefore a book for University courses in Computer Science and Computer Engineering, but the tight proximity of the topics with the industrial practice makes it suitable also as a reference text for designers and engineers of embedded systems industries.
Fantechi A
Embedded systems are becoming more and more pervasive in daily life. Standard hardware/software design techniques can be a sufficient background for the realization of such systems, but the actual design of embedded systems displays multiple critical aspects that deserve to be addressed. Together with the specific techniques for the design of such systems (processors characteristics, real time aspects, etc.), this book introduces concepts such as reliability, availability, safety, and describes the techniques adopted to associate these attributes to a system, with constant reference to the current norms and regulations belonging to various application domains. This book comes from the more than ten years research/teaching experience of the author on these topics, not only in academia, but also in several industrial settings. It is therefore a book for University courses in Computer Science and Computer Engineering, but the tight proximity of the topics with the industrial practice makes it suitable also as a reference text for designers and engineers of embedded systems industries.
See at:
CNR IRIS
2004
Other
Open Access
Applications of Formal Methods for Validating an Interaction Policy
Fantechi A, Gnesi S, Semini L
We describe here an experience in the application of formal methods to the design of fault-tolerant systems. The experience was done inside an applied research project. The input for our validation is an interaction policy between communicating objects, the Multiple Levels of Integrity policy, which has been defined within the project to enhance systems dependability
Fantechi A, Gnesi S, Semini L
We describe here an experience in the application of formal methods to the design of fault-tolerant systems. The experience was done inside an applied research project. The input for our validation is an interaction policy between communicating objects, the Multiple Levels of Integrity policy, which has been defined within the project to enhance systems dependability
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2011
Conference article
Restricted
Model checking interlocking control tables
Ferrari A, Magnani G, Grasso D, Fantechi A
A challenging problem for model checking is represented by railway interlocking systems. It is a well known fact that interlocking systems, due to their inherent complexity related to the high number of variables involved, are not amenable to automatic verifi cation, typically incurring in state space explosion problems. The literature is however quite scarce on data concerning the size of interlocking systems that have been successfully proved with model checking techniques. In this paper we attempt a systematic study of the applicability bounds for general purpose model checkers on this class of systems, by studying the typical characteristics of control tables and their size parameters. The results con firm that, although small scale interlocking systems can be addressed by model checking, interlockings that control medium or large railway yards cannot, asking for specialized verifi cation techniques.DOI: 10.1007/978-3-642-14261-1_11
Metrics:
Ferrari A, Magnani G, Grasso D, Fantechi A
A challenging problem for model checking is represented by railway interlocking systems. It is a well known fact that interlocking systems, due to their inherent complexity related to the high number of variables involved, are not amenable to automatic verifi cation, typically incurring in state space explosion problems. The literature is however quite scarce on data concerning the size of interlocking systems that have been successfully proved with model checking techniques. In this paper we attempt a systematic study of the applicability bounds for general purpose model checkers on this class of systems, by studying the typical characteristics of control tables and their size parameters. The results con firm that, although small scale interlocking systems can be addressed by model checking, interlockings that control medium or large railway yards cannot, asking for specialized verifi cation techniques.DOI: 10.1007/978-3-642-14261-1_11
Metrics:
See at:
doi.org | CNR IRIS | CNR IRIS | www.springerlink.com
2012
Conference article
Restricted
Distributing the challenge of model checking interlocking control tables
Fantechi A
Railway interlocking systems represent a challenge for model checkers: although encoding interlocking rules as finite state machines can be quite straightforward, and safety properties to be proved are easily expressible, the inherent complexity related to the high number of variables involved makes the verification of such systems typically incur state space explosion problems. Domain-specific techniques have been adopted to advance the size of interlocking systems that can be successfully proved, but still not reaching the size needed for large deployment cases. We propose a novel approach in which we exploit a distributed modelling of an interlocking system and a careful selection of verification scenarios, so that parallel verifications conducted on multiple processors can address systems of a large size. Some experiments in this direction are presented and new directions of research according to this proposal are discussed.DOI: 10.1007/978-3-642-34032-1_26
Metrics:
Fantechi A
Railway interlocking systems represent a challenge for model checkers: although encoding interlocking rules as finite state machines can be quite straightforward, and safety properties to be proved are easily expressible, the inherent complexity related to the high number of variables involved makes the verification of such systems typically incur state space explosion problems. Domain-specific techniques have been adopted to advance the size of interlocking systems that can be successfully proved, but still not reaching the size needed for large deployment cases. We propose a novel approach in which we exploit a distributed modelling of an interlocking system and a careful selection of verification scenarios, so that parallel verifications conducted on multiple processors can address systems of a large size. Some experiments in this direction are presented and new directions of research according to this proposal are discussed.DOI: 10.1007/978-3-642-34032-1_26
Metrics:
See at:
doi.org | CNR IRIS | CNR IRIS | www.springerlink.com
2013
Journal article
Restricted
Using Temporal Logic and Model Checking in Automated Recognition of Human Activities for Ambient-Assisted Living
Magherini T, Fantechi A, Nugent C, Vicario E
Automated monitoring and the recognition of activities of daily living (ADLs) is a key challenge in ambient-assisted living (AAL) for the assistance of the elderly. Within this context, a formal approach may provide a means to fill the gap between the low-level observations acquired by sensing devices and the high-level concepts that are required for the recognition of human activities. We describe a system named ARA (Automated Recognizer of ADLs) that exploits propositional temporal logic and model checking to support automated real-time recognition of ADLs within a smart environment. The logic is shown to be expressive enough for the specification of realistic patterns of ADLs in terms of basic actions detected by a sensorized environment. The online model checking engine is shown to be capable of processing a stream of detected actions in real time. The effectiveness and viability of the approach are evaluated within the context of a smart kitchen, where different types of ADLs are repeatedly performed.Source: IEEE TRANSACTIONS ON HUMAN-MACHINE SYSTEMS, vol. 43 (issue 6), pp. 509-521
DOI: 10.1109/tsmc.2013.2283661
Metrics:
Magherini T, Fantechi A, Nugent C, Vicario E
Automated monitoring and the recognition of activities of daily living (ADLs) is a key challenge in ambient-assisted living (AAL) for the assistance of the elderly. Within this context, a formal approach may provide a means to fill the gap between the low-level observations acquired by sensing devices and the high-level concepts that are required for the recognition of human activities. We describe a system named ARA (Automated Recognizer of ADLs) that exploits propositional temporal logic and model checking to support automated real-time recognition of ADLs within a smart environment. The logic is shown to be expressive enough for the specification of realistic patterns of ADLs in terms of basic actions detected by a sensorized environment. The online model checking engine is shown to be capable of processing a stream of detected actions in real time. The effectiveness and viability of the approach are evaluated within the context of a smart kitchen, where different types of ADLs are repeatedly performed.Source: IEEE TRANSACTIONS ON HUMAN-MACHINE SYSTEMS, vol. 43 (issue 6), pp. 509-521
DOI: 10.1109/tsmc.2013.2283661
Metrics:
See at:
IEEE Transactions on Human-Machine Systems | CNR IRIS | ieeexplore.ieee.org | CNR IRIS
2013
Journal article
Open Access
Session types for safe Web service orchestration
Michaux J, Najm E, Fantechi A
We address the general problem of interaction safety in Web service orchestrations. By considering an essential subset of the BPEL orchestration language, we define SeB, a session based style of this subset. We discuss the formal semantics of SeB and present its main properties. We take a new approach to address the formal semantics which is based on a translation into so-called control graphs. Our semantics accounts for BPEL control links and addresses the static semantics that prescribes the valid usage of variables. We also provide the semantics of service configurations. During a session, a client and a service can engage in a complex series of interactions. By means of the provided semantics, we define precisely what is meant by interaction safety. We then introduce session types in order to prescribe the correct orderings of these interactions. Service providers must declare their provided and required session types. We define a typing algorithm that checks if a service orchestration behaves according to its declared provided and required types. Using a subtyping relation defined on session types, we show that any configuration of well-typed service partners with compatible session types are interaction safe, i.e., involved partners never receive unexpected messages.Source: JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, vol. 82 (issue 8), pp. 282-310
DOI: 10.1016/j.jlap.2013.05.004
Metrics:
Michaux J, Najm E, Fantechi A
We address the general problem of interaction safety in Web service orchestrations. By considering an essential subset of the BPEL orchestration language, we define SeB, a session based style of this subset. We discuss the formal semantics of SeB and present its main properties. We take a new approach to address the formal semantics which is based on a translation into so-called control graphs. Our semantics accounts for BPEL control links and addresses the static semantics that prescribes the valid usage of variables. We also provide the semantics of service configurations. During a session, a client and a service can engage in a complex series of interactions. By means of the provided semantics, we define precisely what is meant by interaction safety. We then introduce session types in order to prescribe the correct orderings of these interactions. Service providers must declare their provided and required session types. We define a typing algorithm that checks if a service orchestration behaves according to its declared provided and required types. Using a subtyping relation defined on session types, we show that any configuration of well-typed service partners with compatible session types are interaction safe, i.e., involved partners never receive unexpected messages.Source: JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, vol. 82 (issue 8), pp. 282-310
DOI: 10.1016/j.jlap.2013.05.004
Metrics:
See at:
The Journal of Logic and Algebraic Programming | CNR IRIS | CNR IRIS | www.sciencedirect.com
2013
Contribution to book
Open Access
Some trends in formal methods applications to railway signaling
Fantechi A, Fokkink W, Morzenti A
Railway signaling is often considered as one of the most fruitful areas of intervention by formal methods. This chapter offers insight into the actual industrial usage of formal methods in this field, which does not yet meet the promises of the aforementioned success stories, but is steadily increasing. The external conditions that are driving industrial choices are also discussed. The EN50128 guidelines by the European Committee for Electrotechnical Standardization (CENELEC) regarding the development of software for railway signaling are discussed. The chapter reports on a comparative case study of the applicability of different formal methods to railway signaling. It talks about the applications in the railway domain of one such formal method, namely B. The chapter focuses on formal methods applications to railway signaling equipment, which is divided into train control systems and interlocking systems.DOI: 10.1002/9781118459898.ch4
Metrics:
Fantechi A, Fokkink W, Morzenti A
Railway signaling is often considered as one of the most fruitful areas of intervention by formal methods. This chapter offers insight into the actual industrial usage of formal methods in this field, which does not yet meet the promises of the aforementioned success stories, but is steadily increasing. The external conditions that are driving industrial choices are also discussed. The EN50128 guidelines by the European Committee for Electrotechnical Standardization (CENELEC) regarding the development of software for railway signaling are discussed. The chapter reports on a comparative case study of the applicability of different formal methods to railway signaling. It talks about the applications in the railway domain of one such formal method, namely B. The chapter focuses on formal methods applications to railway signaling equipment, which is divided into train control systems and interlocking systems.DOI: 10.1002/9781118459898.ch4
Metrics:
See at:
www.cs.vu.nl | NARCIS | NARCIS | CNR IRIS | CNR IRIS | onlinelibrary.wiley.com | NARCIS | NARCIS
2013
Conference article
Restricted
Topologically configurable systems as product families
Fantechi A
We address a category of systems whose deployment requires a configuration according to topological information. Although inspired by the case of railway interlocking systems, we give a general definition of topologically configurable control systems. We consider the application of product line engineering principles to the development of these systems, by discussing the adoption of different approaches to achieve a flexible configuration of products, able to factorise most of the design effort, as typical in a product line approach. Verifying the behaviour of such systems, either by testing or by formal verification is actually a challenge: the intricate relations between the actual topology controlled by a product and its functional requirements may prevent any attempt to factorise analysis activities. We will discuss how the application of product line engineering principles can help, with special focus on formal verification, pointing to several open research issues. © 2013 ACM.DOI: 10.1145/2491627.2491643
Metrics:
Fantechi A
We address a category of systems whose deployment requires a configuration according to topological information. Although inspired by the case of railway interlocking systems, we give a general definition of topologically configurable control systems. We consider the application of product line engineering principles to the development of these systems, by discussing the adoption of different approaches to achieve a flexible configuration of products, able to factorise most of the design effort, as typical in a product line approach. Verifying the behaviour of such systems, either by testing or by formal verification is actually a challenge: the intricate relations between the actual topology controlled by a product and its functional requirements may prevent any attempt to factorise analysis activities. We will discuss how the application of product line engineering principles can help, with special focus on formal verification, pointing to several open research issues. © 2013 ACM.DOI: 10.1145/2491627.2491643
Metrics:
See at:
doi.org | CNR IRIS | CNR IRIS | www.scopus.com
2014
Contribution to book
Restricted
Twenty-Five Years of Formal Methods and Railways: What Next?
Fantechi A
Since more than 25 years, railway signalling is the subject of successful industrial application of formal methods in the development and verification of its computerized equipment. However the evolution of the technology of railways signalling systems in this long term has had a strong influence on the way formal methods can be applied in their design and implementation. At the same time important advances had been also achieved in the formal methods area. The scope of the formal methods discipline has enlarged from the methodological provably correct software construction of the beginnings to the analysis and modelling of increasingly complex systems, always on the edge of the ever improving capacity of the analysis tools, thanks to the technological advances in formal verification of both qualitative and quantitative properties of such complex systems. The thesis we will put forward in this paper is that the complexity of future railway systems of systems can be addressed with advantage only by a higher degree of distribution of functions on local interoperable computers - communicating by means of standard protocols - and by adopting a multi-level formal modelling suitable to support the verification at different abstraction levels, and at different life-cycle times, of the safe interaction among the distributed functions.DOI: 10.1007/978-3-319-05032-4_13
Metrics:
Fantechi A
Since more than 25 years, railway signalling is the subject of successful industrial application of formal methods in the development and verification of its computerized equipment. However the evolution of the technology of railways signalling systems in this long term has had a strong influence on the way formal methods can be applied in their design and implementation. At the same time important advances had been also achieved in the formal methods area. The scope of the formal methods discipline has enlarged from the methodological provably correct software construction of the beginnings to the analysis and modelling of increasingly complex systems, always on the edge of the ever improving capacity of the analysis tools, thanks to the technological advances in formal verification of both qualitative and quantitative properties of such complex systems. The thesis we will put forward in this paper is that the complexity of future railway systems of systems can be addressed with advantage only by a higher degree of distribution of functions on local interoperable computers - communicating by means of standard protocols - and by adopting a multi-level formal modelling suitable to support the verification at different abstraction levels, and at different life-cycle times, of the safe interaction among the distributed functions.DOI: 10.1007/978-3-319-05032-4_13
Metrics:
See at:
doi.org | CNR IRIS | CNR IRIS | link.springer.com
2014
Conference article
Restricted
On the validation of an interlocking system by model-checking
Bonacchi A, Fantechi A
Railway interlocking systems still represent a challenge for formal verification by model checking: the high number of complex interlocking rules that guarantee the safe movements of independent trains in a large station makes the verification of such systems typically incur state space explosion problems. In this paper we describe a study aimed to define a verification process based on commercial modelling and verification tools, for industrially produced interlocking systems, that exploits an appropriate mix of environment abstraction, slicing and CEGAR-like techniques, driven by the low-level knowledge of the interlocking product under verification, in order to support the final validation phase of the implemented products. © 2014 Springer International Publishing.DOI: 10.1007/978-3-319-10702-8_7
Metrics:
Bonacchi A, Fantechi A
Railway interlocking systems still represent a challenge for formal verification by model checking: the high number of complex interlocking rules that guarantee the safe movements of independent trains in a large station makes the verification of such systems typically incur state space explosion problems. In this paper we describe a study aimed to define a verification process based on commercial modelling and verification tools, for industrially produced interlocking systems, that exploits an appropriate mix of environment abstraction, slicing and CEGAR-like techniques, driven by the low-level knowledge of the interlocking product under verification, in order to support the final validation phase of the implemented products. © 2014 Springer International Publishing.DOI: 10.1007/978-3-319-10702-8_7
Metrics:
See at:
doi.org | CNR IRIS | CNR IRIS | link.springer.com
1992
Other
Open Access
Multi-way to two-way synchronization
Fantechi A
A process P, in which an action on a gate a can be simultaneously performed by more than two subprocesses, is transformed in an "equivalent" process Q in which each action is performed at most by two subprocesses. That is, the degree of synchronization associated to QD should be at most 2. A variant of this problem imposes a bound on the synchronization degrees relative to a predefined subset of gates. Actually, the formal description of the problem and most of the solutions refer to a single multi-way gate present in P.
Fantechi A
A process P, in which an action on a gate a can be simultaneously performed by more than two subprocesses, is transformed in an "equivalent" process Q in which each action is performed at most by two subprocesses. That is, the degree of synchronization associated to QD should be at most 2. A variant of this problem imposes a bound on the synchronization degrees relative to a predefined subset of gates. Actually, the formal description of the problem and most of the solutions refer to a single multi-way gate present in P.
1999
Journal article
Restricted
GUARDS: a generic upgradable architecture for real-time dependable systems
Powell D, Arlat J, Beusdukic L, Bondavalli A, Coppola P, Fantechi A, Jenn E, Rabejac C, Wellings A
The development and validation of fault-tolerant computers for critical real-time applications are currently both costly and time consuming. Often, the underlying technology is out-of-date by the time the computers are ready for deployment. Obsolescence can become a chronic problem when the systems in which they are embedded have lifetimes of several decades. This paper gives an overview of the work carried out in a project that is tackling the issues of cost and rapid obsolescence by defining a generic fault-tolerant computer architecture based essentially on commercial off-the-shelf (COTS) components (both processor hardware boards and real-time operating systems). The architecture uses a limited number of specific, but generic, hardware and software components to implement an architecture that can be configured along three dimensions: redundant channels, redundant lanes, and integrity levels. The two dimensions of physical redundancy allow the definition of a wide variety of instances with different fault tolerance strategies. The integrity level dimension allows application components of different levels of criticality to coexist in the same instance. The paper describes the main concepts of the architecture, the supporting environments for development and validation, and the prototypes currently being implemented.Source: IEEE TRANSACTIONS ON PARALLEL AND DISTRIBUTED SYSTEMS (PRINT), vol. 10 (issue 6), pp. 580-599
DOI: 10.1109/71.774908
Metrics:
Powell D, Arlat J, Beusdukic L, Bondavalli A, Coppola P, Fantechi A, Jenn E, Rabejac C, Wellings A
The development and validation of fault-tolerant computers for critical real-time applications are currently both costly and time consuming. Often, the underlying technology is out-of-date by the time the computers are ready for deployment. Obsolescence can become a chronic problem when the systems in which they are embedded have lifetimes of several decades. This paper gives an overview of the work carried out in a project that is tackling the issues of cost and rapid obsolescence by defining a generic fault-tolerant computer architecture based essentially on commercial off-the-shelf (COTS) components (both processor hardware boards and real-time operating systems). The architecture uses a limited number of specific, but generic, hardware and software components to implement an architecture that can be configured along three dimensions: redundant channels, redundant lanes, and integrity levels. The two dimensions of physical redundancy allow the definition of a wide variety of instances with different fault tolerance strategies. The integrity level dimension allows application components of different levels of criticality to coexist in the same instance. The paper describes the main concepts of the architecture, the supporting environments for development and validation, and the prototypes currently being implemented.Source: IEEE TRANSACTIONS ON PARALLEL AND DISTRIBUTED SYSTEMS (PRINT), vol. 10 (issue 6), pp. 580-599
DOI: 10.1109/71.774908
Metrics:
See at:
IEEE Transactions on Parallel and Distributed Systems | CNR IRIS | CNR IRIS | www.scopus.com