Verification of Dependable Architecture based on Prototype Verification System
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 relinbility requircments.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.
System Architecture PVS System Fault Tolerance Formal Modeling Formal Verification
Ling Yuan Ping Fan
School of Computer Science Huazhong University of Science and Technology Wuhan, China School of Computer Science Hubei University of science and technology Hubei, China
国际会议
太原
英文
918-921
2012-12-08（万方平台首次上网日期，不代表论文的发表时间）