Verification of Dependable Architecture Based on Prototype Verification System

Abstract:

The electronic power system can be viewed as a system composed of a set of concurrently interacting subsystems to generate, transmit, and distribute electric power. The complex interaction among sub-systems makes the design of electronic power system complicated. Furthermore, in order to guarantee the safe generation and distribution of electronic power, the fault tolerant mechanisms are incorporated in the system design to satisfy high reliability requirements. As a result, the incorporation makes the design of such system more complicated. We propose a dependable electronic power system architecture, which can provide a generic framework to guide the development of electronic power system to ease the development complexity. In order to provide common idioms and patterns to the system designers, we formally model the electronic power system architecture by using the PVS formal language. Based on the PVS model of this system architecture, we formally verify the fault tolerant properties of the system architecture by using the PVS theorem prover, which can guarantee that the system architecture can satisfy high reliability requirements.

• Periodical: Advanced Materials Research (Volumes 756-759)
• Pages: 4188-4192
• DOI: https://doi.org/10.4028/www.scientific.net/AMR.756-759.4188
• Online since: September 2013
• Authors: Ling Yuan, Ping Fan
• Keywords: Fault Tolerance, Formal Modeling, Formal Verification, PVS System, System Architecture

References

[1] M. Shaw, The coming-of-age of software architecture research, Proceedings of the 23rd International Conference on Software Engineering (ICSE 2001), (2001).

DOI: 10.1109/icse.2001.919147

[2] D. Garlan and M. Shaw, Introduction to software arch-itecture, IEEE Transactions on Software Engineering. 1995, 21(4): 269-274.

[3] J.C. Laprie, Dependability basic concepts and terminology, Dependable Computing and Fault Tolerant Systems. Springer-Verlag, (1992).

DOI: 10.1007/978-3-7091-9170-5_1

[4] M. Xie, K.L. Poh, and Y.S. Dai, Computing system reliability: models and analysis, Springer, (2004).

[5] G.T. Leavens and M. Sitaraman, Foundations of component-based systems, Cambridge University Press, (2000).

[6] G.D. Abowd, R. Allen, and D. Garlan, Formalizing style to understand descriptions of software architecture, ACM Transactions on Software Engineering and Methodology, 1995, vol4(4): 319-364.

DOI: 10.1145/226241.226244

[7] J. Sun and J.S. Dong, Specifying and reasoning about generic architecture in TCOZ",. In Proceedings of the 9th Asia-Pacific Software Engineering Conference (APSEC, 02), IEEE Computer Society Press, 2002: 405-414.

DOI: 10.1109/apsec.2002.1183010

[8] M. Shaw and D. Garlan, Software architecture: perspectives on an emerging discipline, Prentice Hall, (1996).

[9] S. Owre and N. Shankar, The formal semantics of PVS, Computer Science Laboratory, SRI International, Menlo Park, CA, (1997).