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 (Online) 35 (2005): 1317–1347. doi:10.1002/spe.673
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 (Online) 35 (2005): 1317–1347. doi:10.1002/spe.673
DOI: 10.1002/spe.673
Metrics:
See at:
Software Practice and Experience 
| onlinelibrary.wiley.com | CNR ExploRA
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 establishedSource: Lecture notes in computer science (2006): 179–189.
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 establishedSource: Lecture notes in computer science (2006): 179–189.
See at:
www.springerlink.com | CNR ExploRA
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.Source: COORDINATION 2008 - Coordination Models and Languages. 10th International Conference, pp. 117–134, Oslo, Norway, 4-6 June 2008
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.Source: COORDINATION 2008 - Coordination Models and Languages. 10th International Conference, pp. 117–134, Oslo, Norway, 4-6 June 2008
DOI: 10.1007/978-3-540-68265-3_8
Metrics:
See at:
Flore (Florence Research Repository) 
| doi.org | link.springer.com | CNR ExploRA
2009
Conference article
Open Access
Formal development for railway signaling using commercial tools
Ferrari A., Fantechi A., Bacherini S., Zingoni N.
This report presents the approach experimented by a railway signaling manufacturer for the development of applications through Simulink/Stateflow in a standard-regulated industrial framework.Source: Formal Methods for Industrial Critical Systems. 14th International Workshop, pp. 197–198, Eindhoven, The Netherlands, 2-3 November 2009
DOI: 10.1007/978-3-642-04570-7_15
Metrics:
Ferrari A., Fantechi A., Bacherini S., Zingoni N.
This report presents the approach experimented by a railway signaling manufacturer for the development of applications through Simulink/Stateflow in a standard-regulated industrial framework.Source: Formal Methods for Industrial Critical Systems. 14th International Workshop, pp. 197–198, Eindhoven, The Netherlands, 2-3 November 2009
DOI: 10.1007/978-3-642-04570-7_15
Metrics:
See at:
flore.unifi.it | Flore (Florence Research Repository) | link.springer.com | doi.org | CNR ExploRA
2009
Contribution to journal
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:
link.springer.com | doi.org | CNR ExploRA
2010
Conference article
Restricted
The Metrô Rio ATP case study
Ferrari A., Grasso D., Magnani G., Fantechi A., Tempestini M.
This paper reports on the Simulink/Stateflow based development of the on-board equipment of the Metrô Rio Automatic Train Protection system. Particular focus is given to the strategies followed to address formal weaknesses and certification issues of the adopted tool-suite. On the development side, constraints on the Simulink/Stateflow semantics have been introduced and design practices have been adopted to gradually achieve a formal model of the system. On the verification side, a two-phase approach based on model based testing and abstract interpretation has been followed to enforce functional correctness and runtime error freedom. Quantitative results are presented to assess the overall strategy: the effort required by the design activities is balanced by the effectiveness of the verification tasks enabled by model based development and automatic code generation.Source: FMICS 2010 - Formal Methods for Industrial Critical Systems. 15th International Workshop, pp. 1–16, Antwerp, Belgium, 20-21 September 2010
DOI: 10.1007/978-3-642-15898-8_1
Metrics:
Ferrari A., Grasso D., Magnani G., Fantechi A., Tempestini M.
This paper reports on the Simulink/Stateflow based development of the on-board equipment of the Metrô Rio Automatic Train Protection system. Particular focus is given to the strategies followed to address formal weaknesses and certification issues of the adopted tool-suite. On the development side, constraints on the Simulink/Stateflow semantics have been introduced and design practices have been adopted to gradually achieve a formal model of the system. On the verification side, a two-phase approach based on model based testing and abstract interpretation has been followed to enforce functional correctness and runtime error freedom. Quantitative results are presented to assess the overall strategy: the effort required by the design activities is balanced by the effectiveness of the verification tasks enabled by model based development and automatic code generation.Source: FMICS 2010 - Formal Methods for Industrial Critical Systems. 15th International Workshop, pp. 1–16, Antwerp, Belgium, 20-21 September 2010
DOI: 10.1007/978-3-642-15898-8_1
Metrics:
See at:
doi.org | www.springerlink.com | CNR ExploRA
2005
Journal article
Unknown
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 60 (2005): 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 60 (2005): 989–1022.
See at: CNR ExploRA
2009
Book
Unknown
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.Source: milano: città studi milano, 2009
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.Source: milano: città studi milano, 2009
See at: CNR ExploRA
2009
Conference article
Open Access
Formal modeling for railway signaling using commercial tools
Ferrari A., Fantechi A., Bacherini S., Zingoni N.
Modeling guidelines constitute one of the fundamental cornerstones for Model Based Development. Their relevance is essential when dealing with code generation in the safety-critical domain. This article presents the experience of a railway signaling systems manufacturer on this issue.Source: The First NASA Formal Methods Symposium, pp. 166–170, Moffett Field, California, April 6 - 8 2009
Ferrari A., Fantechi A., Bacherini S., Zingoni N.
Modeling guidelines constitute one of the fundamental cornerstones for Model Based Development. Their relevance is essential when dealing with code generation in the safety-critical domain. This article presents the experience of a railway signaling systems manufacturer on this issue.Source: The First NASA Formal Methods Symposium, pp. 166–170, Moffett Field, California, April 6 - 8 2009
See at:
ti.arc.nasa.gov | CNR ExploRA
2010
Conference article
Open Access
Model based testing and abstract interpretation in the railway signaling context
Grasso D., Fantechi A., Ferrari A., Becheri C., Bacherini S.
This article presents the experience of a railway signaling manufacturer in introducing the technologies of model based testing and abstract interpretation as part of its development process. Preliminary results show the better performance of these techniques with respect to the previously employed structural coverage based testingSource: Third International Conference on Software Testing, Verification and Validation, Paris, 6-10 April 2010
DOI: 10.1109/icst.2010.44
Metrics:
Grasso D., Fantechi A., Ferrari A., Becheri C., Bacherini S.
This article presents the experience of a railway signaling manufacturer in introducing the technologies of model based testing and abstract interpretation as part of its development process. Preliminary results show the better performance of these techniques with respect to the previously employed structural coverage based testingSource: Third International Conference on Software Testing, Verification and Validation, Paris, 6-10 April 2010
DOI: 10.1109/icst.2010.44
Metrics:
See at:
flore.unifi.it | Flore (Florence Research Repository) | doi.org | ieeexplore.ieee.org | CNR ExploRA
2004
Report
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 dependabilitySource: ISTI Technical reports, pp.1–33, 2004
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 dependabilitySource: ISTI Technical reports, pp.1–33, 2004
See at:
ISTI Repository | CNR ExploRA
2011
Conference article
Closed Access
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.Source: Formal Methods for Automation and Safety in Railway and Automotive Systems 2010 - FORMS/FORMAT 2010, pp. 107–115, Braunschweig, Germany, 2-3 December 2010
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.Source: Formal Methods for Automation and Safety in Railway and Automotive Systems 2010 - FORMS/FORMAT 2010, pp. 107–115, Braunschweig, Germany, 2-3 December 2010
DOI: 10.1007/978-3-642-14261-1_11
Metrics:
See at:
doi.org | www.springerlink.com | CNR ExploRA
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.Source: Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies - 5th International Symposium, pp. 276–289, Heraclion, Crete, 15-18 October 2012
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.Source: Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies - 5th International Symposium, pp. 276–289, Heraclion, Crete, 15-18 October 2012
DOI: 10.1007/978-3-642-34032-1_26
Metrics:
See at:
doi.org | www.springerlink.com | CNR ExploRA
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 Systems Man and Cybernetics Part C-Applications and Reviews 43 (2013): 509–521. doi:10.1109/TSMC.2013.2283661
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 Systems Man and Cybernetics Part C-Applications and Reviews 43 (2013): 509–521. doi:10.1109/TSMC.2013.2283661
DOI: 10.1109/tsmc.2013.2283661
Metrics:
See at:
IEEE Transactions on Human-Machine Systems | ieeexplore.ieee.org | CNR ExploRA
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: The journal of logic and algebraic programming 82 (2013): 282–310. doi:10.1016/j.jlap.2013.05.004
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: The journal of logic and algebraic programming 82 (2013): 282–310. doi:10.1016/j.jlap.2013.05.004
DOI: 10.1016/j.jlap.2013.05.004
Metrics:
See at:
The Journal of Logic and Algebraic Programming | www.sciencedirect.com | CNR ExploRA
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.Source: Formal Methods for Industrial Critical Systems: A Survey of Applications, edited by Stefania Gnesi, Tiziana Margaria, pp. 61–84, 2013
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.Source: Formal Methods for Industrial Critical Systems: A Survey of Applications, edited by Stefania Gnesi, Tiziana Margaria, pp. 61–84, 2013
DOI: 10.1002/9781118459898.ch4
Metrics:
See at:
www.cs.vu.nl | NARCIS | NARCIS | onlinelibrary.wiley.com | NARCIS | NARCIS | CNR ExploRA
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.Source: SPLC 2013 - 17th International Software Product Line Conference, pp. 151–156, Tokyo, Japan, 26 - 30 August 2013
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.Source: SPLC 2013 - 17th International Software Product Line Conference, pp. 151–156, Tokyo, Japan, 26 - 30 August 2013
DOI: 10.1145/2491627.2491643
Metrics:
See at:
doi.org | www.scopus.com | CNR ExploRA
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.Source: Software Engineering and Formal Methods, edited by Steve Counsell, Manuel Núñez, pp. 167–183, 2014
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.Source: Software Engineering and Formal Methods, edited by Steve Counsell, Manuel Núñez, pp. 167–183, 2014
DOI: 10.1007/978-3-319-05032-4_13
Metrics:
See at:
doi.org | link.springer.com | CNR ExploRA
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.Source: FMICS 2014 - Formal Methods for Industrial Critical Systems. 19th International Conference, pp. 94–108, Florence, Italy, 11-12 September 2014
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.Source: FMICS 2014 - Formal Methods for Industrial Critical Systems. 19th International Conference, pp. 94–108, Florence, Italy, 11-12 September 2014
DOI: 10.1007/978-3-319-10702-8_7
Metrics:
See at:
doi.org | link.springer.com | CNR ExploRA
1992
Other
Unknown
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.
See at: CNR ExploRA