Verification of Dependable Architecture based on Prototype Verification System

DOI

10.2991/iccia.2012.223How to use a DOI?

Keywords

System Architecture, PVS System, Fault Tolerance, Formal Modeling, Formal Verification.

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.

Copyright

© 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/).

Download article (PDF)

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  - 10.2991/iccia.2012.223
ID  - Yuan2014/05
ER  -