Component-Based Modeling and Observer-Based Verification for Railway Safety-Critical Applications

详细信息    查看全文

• 作者：Marc Sango (15) (16)
  Laurence Duchien (16)
  Christophe Gransart (15)
  
• 关键词：Software component ; Timed automata ; Transformation ; Verification ; Safety ; critical applications
• 刊名：Lecture Notes in Computer Science
• 出版年：2015
• 出版时间：2015
• 年：2015
• 卷：8997
• 期：1
• 页码：248-266
• 全文大小：2,434 KB
• 参考文献：1. Adler, R., Schaefer, I., Trapp, M., Poetzsch-Heffter, A.: Component-based modeling and verification of dynamic adaptation in safety-critical embedded systems. ACM Trans. Embed. Comput. Syst. 10(2), 20:1鈥?0:39 (2011)
  2. Akerholm, M., Moller, A., Hansson, H., Nolin, M.: Towards a dependable component technology for embedded system applications. In: 10th International Workshop on Object-Oriented Real-Time Dependable Systems, pp. 320鈥?28, February 2005
  3. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183鈥?35 (1994) CrossRef
  4. Bhatti, Z., Sinha, R., Roop, P.: Observer based verification of iec 61499 function blocks. In: Industrial Informatics (INDIN), pp. 609鈥?14, July 2011
  5. Crnkovic, I., Sentilles, S., Vulgarakis, A., Chaudron, M.R.V.: A classification framework for software component models. IEEE Trans. Softw. Eng. 37(5), 593鈥?15 (2011) CrossRef
  6. Dong, J.S., Hao, P., Qin, S., Sun, J., Yi, W.: Timed automata patterns. IEEE Trans. Softw. Eng. 34(6), 844鈥?59 (2008) CrossRef
  7. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of ICSE鈥?9, pp. 411鈥?20 (1999)
  8. EN-50128. Railway applications鈥攃ommunication, signalling and processing systems鈥攕oftware for railway control and protection systems, January 2011
  9. Hi-lite. Simplifying the use of formal methods: verification by contract. http://www.open-do.org/projects/hi-lite/
  10. IEC-61499. IEC 61499 function blocks for industrial-process measurement and control systems. Geneva, Switzerland (2005)
  11. Kaynar, D.K., Lynch, N., Segala, R., Vaandrager, F.: The Theory of Timed I/O Automata. Morgan & Claypool Publishers, Cambridge (2006)
  12. Konrad, S., Cheng, B.H.C.: Real-time specification patterns. In: Proceedings of the 27th ICSE, pp. 372鈥?81 (2005)
  13. Krichen, M., Tripakis, S.: Conformance testing for real-time systems. Form. Methods Syst. Des. 34(3), 238鈥?04 (2009) CrossRef
  14. Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1鈥?), 134鈥?52 (1997) CrossRef
  15. Mekki, A., Ghazel, M., Toguyeni, A.: Validation of a new functional design of automatic protection systems at level crossings with model-checking techniques. IEEE Trans. Intell. Transp. Syst. 13(2), 714鈥?23 (2012) CrossRef
  16. Sango, M.: Application of sara approach to ertms/etcs on-board train control system. Technical report, IFSTTAR, April 2013. http://urls.fr/sara
  17. Sango, M., Gransart, C., Duchien, L.: Safety component-based approach and its application to ERTMS/ETCS on-board train control system. In: TRA2014 Transport Research Arena 2014, Paris, France, April 2014
  18. Sendall, S., Kozaczynski, W.: Model transformation: The heart and soul of model-driven software development. IEEE Softw. 20(5), 42鈥?5 (2003) CrossRef
  19. Soliman, D., Thramboulidis, K., Frey, G.: Transformation of function block diagrams to uppaal timed automata for the verification of safety applications. Ann. Rev. Control 36(2), 338鈥?45 (2012) CrossRef
  20. Szyperski, C.: Component Software: Beyond Object-Oriented Programming. Addison-Wesley Longman Publishing Co. Inc., Boston (1998)
  21. Tamura, G., Casallas, R., Cleve, A., Duchien, L.: Qos contract-aware reconfiguration of component architectures using e-graphs. In: FACS鈥?0, pp. 34鈥?2 (2010)
  22. Taylor, K.: Addressing road user behavioural changes at railway level crossings. In: ACRS-Travelsafe National Conference, pp. 368鈥?75, Brisbane, Australia (2008)
  23. Whittle, J.: Specifying precise use cases with use case charts. In: Bruel, J.-M. (ed.) MoDELS 2005. LNCS, vol. 3844, pp. 290鈥?01. Springer, Heidelberg (2006) CrossRef
  24. Yovine, S.: A verification tool for real-time systems. Int. J. Softw. Tools Technol. Transf. 1(1鈥?), 123鈥?33 (1997). Springer CrossRef
  
• 作者单位：Marc Sango (15) (16)
  Laurence Duchien (16)
  Christophe Gransart (15)
  
  15. IFSTTAR, COSYS/LEOST, 59650, Villeneuve-d鈥橝scq, France
  16. INRIA Lille-Nord Europe, LIFL CNRS UMR 8022, University of Lille 1, 59650, Villeneuve-d鈥橝scq, France
  
• 丛书名：Formal Aspects of Component Software
• ISBN：978-3-319-15317-9
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

One of the challenges that engineers face, during the development process of safety-critical systems, is the verification of safety application models before implementation. Formalization is important in order to verify that the design meets the specified safety requirements. In this paper, we formally describe the set of transformation rules, which are defined for the automatic transformation of safety application source models to timed automata target models. The source models are based on our domain-specific component model, named SARA, dedicated to SAfety-critical RAilway control applications. The target models are then used for the observer-based verification of safety requirements. This method provides an intuitive way of expressing system properties without requiring a significant knowledge of higher order logic and theorem proving, as required in most of existing approaches. An experimentation over a chosen benchmark at rail-road crossing protection application is shown to highlight the proposed approach.