Automatic Timed Automata Extraction from Ladder Programs for Model-Based Analysis of Control Systems

Automatic Timed Automata Extraction from Ladder Programs for Model-Based Analysis of Control Systems

Kézia Oliveira (Federal University of Campina Grande. Campina Grande, Brazil), Kyller Gorgônio (Federal University of Campina Grande. Campina Grande, Brazil), Angelo Perkusich (Federal University of Campina Grande. Campina Grande, Brazil), Antônio Lima (Federal University of Campina Grande. Campina Grande, Brazil) and Leandro Dias da Silva (Computing Institute Federal University of Alagoas,Brazil)
Copyright: © 2011 |Pages: 24
DOI: 10.4018/978-1-61520-837-1.ch012
OnDemand PDF Download:
Available
$37.50
Current Special Offers
No Current Special Offers
TOTAL SAVINGS: $37.50

Abstract

Control Systems are used to produce a certain result with little or no human supervision. The principal aim of such systems is to ensure that resources are used efficiently and that the desired product quality is achieved. Moreover for critical systems such as oil and gas plants, it is important to guarantee the safety and dependability of the operation. Therefore, it is necessary to verify whether what is running in the device is in accordance with what was defined in the specification documents. The goal of this chapter is to present a method that automatically generates the timed automata models from the specification ISA 5.2 Binary Logic Diagrams, and the implementation Ladder programs, for model-based analysis, in order to increase the confidence in the behavior of critical Control Systems. This approach is based on the use of the Uppaal tool and the Uppaal-TRON testing tool.
Chapter Preview
Top

Background

In this section the theoretical basis necessary for the understanding of this chapter is presented. The main concepts related to ISA 5.2 Binary Logic Diagrams (ISA, 1992), Programmable Logic Controllers (PLC), Ladder and timed automata are introduced.

Complete Chapter List

Search this Book:
Reset