Verification of Dependable Architecture based on Prototype Verification System
- https://doi.org/10.2991/iccia.2012.223How to use a DOI?
- System Architecture, PVS System, Fault Tolerance, Formal Modeling, Formal Verification.
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.
- © 2013, the Authors. Published by Atlantis Press.
- Open Access
- This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).
Cite this article
TY - CONF AU - Ling Yuan AU - Ping Fan PY - 2014/05 DA - 2014/05 TI - Verification of Dependable Architecture based on Prototype Verification System BT - Proceedings of the 2012 2nd International Conference on Computer and Information Application (ICCIA 2012) PB - Atlantis Press SP - 918 EP - 921 SN - 1951-6851 UR - https://doi.org/10.2991/iccia.2012.223 DO - https://doi.org/10.2991/iccia.2012.223 ID - Yuan2014/05 ER -