Proceedings of the 2012 2nd International Conference on Computer and Information Application (ICCIA 2012)

Verification of Dependable Architecture based on Prototype Verification System

Authors
Ling Yuan, Ping Fan
Corresponding Author
Ling Yuan
Available Online May 2014.
DOI
https://doi.org/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)

Volume Title
Proceedings of the 2012 2nd International Conference on Computer and Information Application (ICCIA 2012)
Series
Advances in Intelligent Systems Research
Publication Date
May 2014
ISBN
978-94-91216-41-1
ISSN
1951-6851
DOI
https://doi.org/10.2991/iccia.2012.223How to use a DOI?
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/).

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  -