VHS - Verification of Hybrid Systems
|
|---|
| Participants | |
|---|---|
| Yassine Lakhnech (now VERIMAG) | |
| Sébastien Bornot | |
| Ralf Huuck | |
| Ben Lukoschus |
| 1st Year Work |
|---|
| 2nd Year Work |
|---|
| Abstract |
|---|
In order to come up with verification tools a solid understanding and a well-defined framework is essential. In 1993 the IEC 1131-3 standard was introduced for PLC programming languages. This standard served as a basis for our work. Moreover, in our point of view a verification tool has not only be compliant to the standard but must be able to handle large amounts of code in order to cope with industrial size programs and it must be usable by engineers who have no background in formal methods, too.
This motivated us to develop a framework and a tool for statically analyzing Programmable Logic Controllers. In particular we focused on the programming language Instruction List (IL). The tool is currently in progress and first encouraging results are expected in the near future. In parallel we worked on a method to automatically model-check the structuring programming language Sequential Function Charts (SFC). For the future we target to combine both tools to get the best of both worlds.
| Progress |
|---|
| Publications |
|---|
Abstract. Programmable logic controllers (PLCs) occupy a big share in automation control. However, hardly any validation tools for their software are available. In this work we present a lightweight verification technique for PLC programs. In particular, static analysis is applied to programs written in Instruction List, a standardized language commonly used for PLC programming. We illustrate how these programs are annotated automatically by an abstract interpretation algorithm which is guaranteed to terminate and is applicable to large-scale programs. The resulting annotations allow static checking for possible run-time errors and provide information about the program structure, like existence of dead code or infinite loops, which in combination contributes to more reliable PLC systems.
[gzip-compressed PostScript file: ADPM2000.ps.gz]
Sébastien Bornot, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus.
An Abstract Model For Sequential Function Charts.
Accepted at the WODES 2000 special session ``Formal Models of PLCs'',
Gent, Belgium, August 21-23, 2000.
Abstract. Sequential function charts (SFCs) are systems where every step can contain other SFCs as well as state transformations. The standard by IEC 1131-3 explicitly defines some languages for this. In this paper we point out that the standard has many ambiguities, and that it is crucial to have a formal framework for the definition of SFCs. We define the syntax and semantics of them. The semantics we give is general enough to cope with different possible implementations of the standard.
[gzip-compressed PostScript file: WODES2000.ps.gz]
Sébastien Bornot, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus.
Verification of Sequential Function Charts using SMV.
Accepted at the PDPTA 2000 special session on Formal Validation, Las
Vegas, Nevada, USA, June 26-29, 2000.
Abstract. Sequential function charts (SFCs) are defined as a modeling language in the IEC 1131-3 standard and can be used to structure and drive programmable logic controllers (PLCs). It includes interesting concepts as hierarchy, history variables and priority. As the typical application area of this language is the control of industrial processes, it is obvious that safety and reliability is a crucial goal for systems using SFCs. In this work we give an abstract formal model for SFCs and present a method to automatically verify properties concerning the safety of such systems using the model checking tool SMV (Symbolic Model Verifier).
[gzip-compressed PostScript file: PDPTA2000.ps.gz]
Sébastien Bornot, Ralf Huuck, Ben Lukoschus.
Statische Analysetechniken für speicherprogrammierbare Steuerungen.
FBT 2000 - 10. GI/ITG-Fachgespräch ``Formale Beschreibungstechniken'' der
Gesellschaft für Informatik (GI), Informationstechnische Gesellschaft im VDE
(ITG), Fachgruppe ``Kommunikation und Verteilte Systeme'',
Lübeck, Germany, June 22/23, 2000.
Zusammenfassung. Speicherprogrammierbare Steuerungen (SPS) unterliegen einer stark zunehmenden Verbreitung in der Automatisierungstechnik. Während diese in der Vergangenheit meist nur zur Steuerung einfacher Abläufe eingesetzt wurden, sind sie heutzutage verantwortlich für die Steuerung komplexer hybrider Systeme, sei es in der petrochemischen Industrie oder in Kraftwerken. Daher ist eine korrekt funktionierende Steuerungssoftware von grundsätzlicher Bedeutung. In diesem Vortrag wird die Methode der statischen Analyse für eine standardisierte SPS-Sprache, Anweisungsliste (AWL), vorgestellt. Statische Analyse umfaßt Techniken, die Laufzeitverhalten ermitteln bzw. nachweisen, ohne den Code selbst auszuführen. Insbesondere die Technik der abstrakten Interpretation spielt hier eine wichtige Rolle. Wir werden diese Techniken mit Bezug auf AWL vorstellen und aufzeigen, welche statischen Analyseziele für AWL erreichbar sind. Ferner gehen wir darauf ein, was statische Analyse im Vergleich zu anderen Verifikationstechniken leistet und wie diese in Kombination genutzt werden können.
[gzip-compressed PostScript file: FBT2000.ps.gz]
| Talks |
|---|
| Other Resources |
|---|
Ralf Huuck
(rhu@informatik.uni-kiel.de)