Scenario-oriented reverse engineering of complex railway system specifications
Abstract
In this article, we present a scenario-oriented modeling methodology dedicated to the analysis and the formalization of complex system specifications. The methodology relies on the SCOLA semiformal notation to describe scenarios and on a formal execution model described in the AltaRica 3.0 modeling language. We designed this methodology because we had to review thousands of pages of natural language specifications of a railway system in view of their validation with respect to safety constraints. We needed therefore some means to understand what the system was supposed to be and to do as well as to support a dialog with experts. This article aims at introducing the methodology and the modeling formalism that supports it as well as at discussing its application to the railway systems.
References
[1]
Issad M, Kloul L, Rauzy A. A model-based methodology to formalize specifications of railway systems. In: Proceedings of the 4th International Symposium on Model-Based Safety Assessment, IMBSA 2014, volume 8822 of LNCS, pages 28-42, October 2014; Munich, Germany: Springer Verlag.
[2]
Issad M, Kloul L, Rauzy A, Berkani K. Modeling the CBTC railway system with SCOLA. In: Proceedings of the 22th ITS World Congress, Bordeaux, France, October 2015, pages 459-467; Ertico - ITS Europe.
[3]
Mortada H, Prosvirnova T, Rauzy A. Safety assessment of an electrical system. In: Proceedings of the 4th International Symposium on Model-Based Safety Assessment, IMBSA 2014, volume 8822 of LNCS, pages 181-194, October 2014; Munich, Germany: Springer Verlag.
[4]
Prosvirnova T. AltaRica 3.0: a Model-Based Approach for Safety Analyses. Thèse de doctorat, École Polytechnique, Palaiseau, France, November 2014.
[5]
Prosvirnova T, Batteux M, Brameret PA, et?al. The altarica 3.0 project for model-based safety assessment. In: Proceedings of 4th IFAC Workshop on Dependable Control of Discrete Systems, DCDS'2013, pages 127-132, September 2013; Elsevier: York, Great Britain. International Federation of Automatic Control.
[6]
IEEE. Standard for Communications Based Train Control CBTC Performance and Functional Requirements. IEEE Std 1474.1-2004 Revision of IEEE Std 1474.1-1999. IEEE, 2004.
[7]
Schmelzer C. Standardization of cbtc systems-mixed operation on shared lines in accordance with ertms/etcs standards, 2008.
[8]
Böhm W, Junker M, Vogelsang A, Teufl S, Pinger R, Rahn K. A formal systems engineering approach in practice: an experience report. In: Proceedings of the 1st International Workshop on Software Engineering Research and Industrial Practices, SER&IPs 2014, pages 34-41, June 2014; Hyderabad, India. ACM.
[9]
Teufl S, Böhm W, Pinger R. Understanding and closing the gap between requirements on system and subsystem level. In: Proceedings 4th International Conference on Model-Driven Requirements Engineering Workshop MoDRE, pages 77-86, August 2014; Karlskrona, Sweden, IEEE.
[10]
Weilkiens T, Lamm J, Roth S, Walker M. Model-Based System Architecture. Wiley Series in Systems Engineering and Management. Hoboken, NJ: Wiley-Blackwell; 2015.
[11]
Abrial JR. The B Book: Assigning Programs to Meanings. Cambridge, England: Cambridge University Press; 2005.
[12]
Friedenthal S, Moore A, Steiner R. A Practical Guide to SysML: The Systems Modeling Language. San Francisco, CA: Morgan Kaufmann, The MK/OMG Press; 2011.
[13]
Milner R. Communication and Concurrency. Prentice-Hall international series in computer science. Upper Saddle River, NJ: Prentice Hall; 1989.
[14]
Hoare CAR. Communicating sequential processes. Commun ACM. 1978; Volume 21 Issue 8: pp.666-677.
[15]
Batteux M, Prosvirnova T, Rauzy A. System Structure Modeling Language S2ML. AltaRica Association; 2015. archive hal-01234903, version 1.
[16]
Noble J, Taivalsaari A, Moore I. Prototype-Based Programming: Concepts, Languages and Applications. Berlin, Heidelberg, Germany: Springer-Verlag; 1999.
[17]
Fowler M. Domain Specific Languages. Boston, MA: Addison-Wesley; 2010.
[18]
Parr T. The definitive ANTLR reference: building domain-specific languages. Pragmatic Programmers, 2013.
[19]
Harel D, Marelly R. Come Let's Play. Berlin, Germany: Springer; 2003.
[20]
Harel D. Statecharts: a visual approach to complex systems. Sci Comput Program. 1987 ;Volume 8 Issue 3: pp.231-274.
[21]
Dori D. Object-Process Methodology -A Holistic Systems Paradigm. Berlin, Heidelberg/New York: Springer Verlag; 2002.
[22]
White S, Miers D. BPMN Modeling and Reference Guide: Understanding and Using BPMN. Lighthouse Point, FL: Future Strategies Inc.; 2008.
[23]
Vogelsang A, Eder S, Hackenberg G, Junker M, Teufl S. Supporting concurrent development of requirements and architecture: a model-based approach. In: Proceedings 2nd International Conference on Model-Driven Engineering and Software Development MODELSWARD, pages 587-595, January 2014; Lisbon, Portugal. IEEE.
[24]
Rauzy A. Guarded transition systems: a new states/events formalism for reliability studies. J Risk Reliab. 2008 ;Volume 222 Issue 4: pp.495-505.
[25]
Eshuis R. Reconciling statechart semantics. Sci Comput Program. 2009; Volume 74: pp.65-99.
[26]
Cockburn A. Writing Effective Use Cases. Boston, MA: Addison Wesley; 2000.
[27]
Wirth N. Algorithms + Data Structures = Programs. Upper Saddle River, NJ: Prentice-Hall; 1976.
[28]
Halbwachs N, Caspi P, Raymond P, Pilaud D. The synchronous dataflow programming language lustre. Proc IEEE. 1991 ;Volume 79 Issue 9: pp.1305-1320.
[29]
Fritzson P. Principles of Object-Oriented Modeling and Simulation with Modelica 2.1. Hoboken, NJ: Wiley-IEEE Press; 2003.
[30]
Abadi M, Cardelli L. A Theory of Objects. New-York: Springer-Verlag; 1998.
[31]
Fuhrmann HAL. On the Pragmatics of Graphical Modeling. Kiel Computer Science Series. Norderstedt, Germany: Book on Demand; 2011.
[32]
Blanchard BS, Fabrycky WJ. Systems Engineering and Analysis. Vol. 4. Englewood Cliffs, NJ: Prentice Hall; 1990.
[33]
INCOSE. INCOSE Systems Engineering Handbook: A Guide for System Life Cycle Processes and Activities. 4th ed. Hoboken, NJ: Wiley-Blackwell; 2015.
[34]
Rumbaugh J, Jacobson I, Booch G. The Unified Modeling Language Reference Manual. Boston, MA: Addison Wesley; 2005.
[35]
Abelson H, Sussman GJ, Sussman J. Structure and Interpretation of Computer Programs. Cambridge, MA: MIT Press; 1996.
[36]
Batteux M, Prosvirnova T, Rauzy A. Altarica 3.0 assertions: the why and the wherefore. J Risk Reliab. 2016. Submitted.
[37]
Ajmone-Marsan M, Balbo G, Conte G, Donatelli S, Franceschinis G. Modelling with Generalized Stochastic Petri Nets. Wiley Series in Parallel Computing. New York, NY: John Wiley and Sons; 1994.
[38]
Vaandrager FW. On the relationship between process algebra and input/output automata. In: LICS'91., Proceedings of Sixth Annual IEEE Symposium on Logic in Computer Science, pages 387-398, 1991, IEEE.
[39]
Baeten JCM. A brief history of process algebra. Theor Comput Sci. 2005; Volume 335 Issue 2: pp.131-146.
[40]
Hopcroft JE. Introduction to Automata Theory, Languages, and Computation. Pearson Education India; 1979.
[41]
Linz P. An Introduction to Formal Languages and Automata. Burlington, MA: Jones & Bartlett Publishers; 2011.
[42]
Bergstra JA, Klop JW. Fixed point semantics in process algebras. Mathematisch Centrum, 1982.
[43]
Hoare CAR. Communicating Sequential Processes. Berlin/New York: Springer; 1978.
[44]
Milner R. A Calculus of Communicating Systems. Berlin/New York: Springer-Verlag; 1980.
[45]
Bergstra JA, Klop JW. Process algebra for synchronous communication. Inform Control. 1984 ;Volume 60 Issue 1-3: pp.109-137.
[46]
Milner R. Calculi for synchrony and asynchrony. Theor Comput Sci., 1983; Volume 25 Issue 3: pp.267-310.
[47]
Milne GJ. Circal and the representation of communication, concurrency, and time. ACM Trans Program Lang Syst. 1985 ;Volume 7 Issue 2: pp.270-298.
[48]
Austry D, Boudol G. Algebre de processus et synchronisation. Theor Comput Sci. 1984 ;Volume 30 Issue 1: pp.91-131.
[49]
Hennessy M. Algebraic Theory of Processes. Cambridge, MA: MIT Press; 1988.
[50]
Glinz M. An integrated formal model of scenarios based on statecharts. In Software Engineering ESEC'95. Berlin/New York: Springer; 1995: pp.254-271.
[51]
Weilkiens T. Systems Engineering with SysML/UML: Modeling, Analysis, Design. San Francisco, CA: Morgan Kaufmann; 2011.
[52]
Mendling J. Event-Driven Process Chains EPC. Berlin/New York: Springer; 2008.
[53]
Murata T. Petri nets: properties, analysis and applications. Proc IEEE. 1989; Volume 77 Issue 4: pp.541-580.
[54]
Alur R, Holzmann GJ, Peled D. An analyzer for message sequence charts. In: Tools and Algorithms for the Construction and Analysis of Systems. Berlin/New York: Springer; 1996: pp.35-48.
[55]
Mauw S. The formalization of message sequence charts. Comput Network ISDN Syst. 1996 ;Volume 28 Issue 12: pp.1643-1657.
[56]
Wong PYH, Gibbons J. A process semantics for BPMN. In: Formal Methods and Software Engineering. Berlin/New York: Springer; 2008: pp.355-374.
[57]
Harel D, Naamad A. The statemate semantics of statecharts. ACM Trans Soft Eng Methodol. 1996 ;Volume 5 Issue 4: pp.293-333.
[58]
Harel D. On the formal semantics of statecharts. In: Proceedings of the 2nd IEEE Symposium on Logic in Computer Science, 1987, pages pp.54-64.
[59]
<familyNamePrefix>von der</familyNamePrefix>Beeck M. A concise compositional statecharts semantics definition. In: Formal Methods for Distributed System Development. Berlin/New York: Springer; 2000: pp.335-350.
[60]
Dijkman RM, Dumas M, Ouyang C. Formal semantics and analysis of BPMN process models using Petri nets. Queensland University of Technology; 2007. Technical Report.
[61]
Raedts I, Petkovic M, Usenko YS, van der Werf JM, Groote JF, and Somers LJ. Transformation of BPMN models for behaviour analysis. In: Proceedings of MSVVEIS, 2007, pages pp.126-137.
[62]
Guelfi N, Mammar A. A formal semantics of timed activity diagrams and its promela translation. In APSEC'05: 12th Asia-Pacific Proceedings of Software Engineering Conference, 2005; Piscataway, NJ: IEEE.
[63]
López-Grao JP, Merseguer J, Campos J. From UML activity diagrams to stochastic Petri nets: application to software performance Engineering. ACM SIGSOFT Softw Eng Notes. 2004 ;Volume 29 Issue 1: pp.25-36.
Recommendations
A formal automated approach for reverse engineering programs with pointers
ASE '97: Proceedings of the 12th international conference on Automated software engineering (formerly: KBSE)Given a program S and a precondition Q, the strongest postcondition, denoted sp(S,Q), is defined as the strongest condition that holds after the execution of S, given that S terminates. By defining the formal semantics of each of the constructs of a ...
An overview of CAFE specification environment-an algebraic approach for creating, verifying, and maintaining formal specifications over networks
ICFEM '97: Proceedings of the 1st International Conference on Formal Engineering MethodsCAFE is the name of a network based environment now under development for supporting systematic creation, checking, verification, and maintenance of formal specifications. CAFE has an algebraic specification language called CafeOBJ as its main ...
Visualization of Formal Specifications
APSEC '99: Proceedings of the Sixth Asia Pacific Software Engineering ConferenceFormal specification techniques provide precise and analyzable software specifications. However, formal notations provided by most formal specification techniques are not easy to use and understand for most people. Our approach counters this difficulty ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Publisher
John Wiley and Sons Ltd.
United Kingdom
Publication History
Published: 01 March 2018
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 29 Sep 2024
Other Metrics
Citations
View Options
View options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in