CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Verification of Process Operations Using Model Checking

Alexey Voronov (Institutionen för signaler och system, Automation) ; Knut Åkesson (Institutionen för signaler och system, Automation)
Automation Science and Engineering, 2009. CASE 2009. IEEE International Conference on p. 415-420. (2009)
[Konferensbidrag, refereegranskat]

In order to decrease time to market for products it is important to decrease the time for implementation and debugging of the control logic that are used to manufacture the products. In this paper, an approach based on a high-level specification of the relations between process operations and resources and the use of formal verification is presented. By using formal verification it is possible to find potential errors within the specification at an early stage in the development process. In this work it is shown how the high-level specifications may be translated into extended finite automata, and how these extended finite automata may be efficiently verified using the symbolic model checking tool, NuSMV. It is also shown how the presented approach is suitable for verification of general supervisory control properties like controllability and non-blocking.

Nyckelord: formal verification, model checking, industrial automation

Article number 523410

Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2009-10-08. Senast ändrad 2016-07-26.
CPL Pubid: 99888


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för signaler och system, Automation (2005-2017)


Datavetenskap (datalogi)

Chalmers infrastruktur

Relaterade publikationer

Denna publikation ingår i:

Using Formal Methods for Product and Production Development -- Industrial Applications for Boolean Satisfiability Solvers