Formal verification of control software: A case study

Andreas Griesmayer; Roderick Paul Bloem; Martin Hautzendorfer; Franz Wotawa

doi:10.1007/11504894_108

Formal verification of control software: A case study

Andreas Griesmayer
, Roderick Paul Bloem
, Martin Hautzendorfer
, Franz Wotawa

Institute of Software Engineering and Artificial Intelligence (7160)

Publikation: Beitrag in Buch/Bericht/Konferenzband › Beitrag in einem Konferenzband › Begutachtung

Abstract

We present a case study of formal verification of control logic for a robotic handling system. We have implemented a system in which properties can be specified in the source code, which is then automatically converted to Java and checked using Java Path Finder. The model checker, working under the assumption of a nondeterministic environment, is able to efficiently verify critical properties of the design.

Originalsprache	englisch
Titel	Innovations in Applied Artificial Intelligence
Untertitel	IEA/AIE 2005
Redakteure/-innen	Moonis Ali
Erscheinungsort	Berlin [u.a.]
Herausgeber (Verlag)	Springer
Seiten	783-788
ISBN (Print)	3-540-26551-1
DOIs	https://doi.org/10.1007/11504894_108
Publikationsstatus	Veröffentlicht - 2005
Veranstaltung	18th International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems: IEA/AIE 2005 - Bari, Italien Dauer: 22 Juni 2005 → 24 Juni 2005

Publikationsreihe

Name	Lecture Notes in Computer Science
Herausgeber (Verlag)	Springer
Band	3533

Konferenz

Konferenz	18th International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems
Kurztitel	IEA/AIE 2005
Land/Gebiet	Italien
Ort	Bari
Zeitraum	22/06/05 → 24/06/05

Treatment code (Nähere Zuordnung)

Experimental

Zugriff auf Dokument

10.1007/11504894_108

veridacs.pdfAkzeptiertes Autorenmanuskript, 75,3 KB

1 Abgeschlossen

EU - Prosyd - Property-Based System Design
Jobstmann, B. (Teilnehmer / Mitarbeiter), Bloem, R. (Projektleiter), Pill, I. H. (Teilnehmer / Mitarbeiter), Griesmayer, A. (Teilnehmer / Mitarbeiter) & Staber, S. S. (Teilnehmer / Mitarbeiter)
1/01/04 → 31/12/06
Projekt: Forschungsprojekt

Dieses zitieren

Formal verification of control software: A case study. / Griesmayer, Andreas; Bloem, Roderick Paul; Hautzendorfer, Martin et al.
Innovations in Applied Artificial Intelligence: IEA/AIE 2005. Hrsg. / Moonis Ali. Berlin [u.a.]: Springer, 2005. S. 783-788 (Lecture Notes in Computer Science ; Band 3533).

Publikation: Beitrag in Buch/Bericht/Konferenzband › Beitrag in einem Konferenzband › Begutachtung

Griesmayer, A, Bloem, RP, Hautzendorfer, M & Wotawa, F 2005, Formal verification of control software: A case study. in M Ali (Hrsg.), Innovations in Applied Artificial Intelligence: IEA/AIE 2005. Lecture Notes in Computer Science , Bd. 3533, Springer, Berlin [u.a.], S. 783-788, 18th International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems, Bari, Italien, 22/06/05. https://doi.org/10.1007/11504894_108

@inproceedings{fbf810f16c994fb88f2b27e7d1cb76ca,

title = "Formal verification of control software: A case study",

abstract = "We present a case study of formal verification of control logic for a robotic handling system. We have implemented a system in which properties can be specified in the source code, which is then automatically converted to Java and checked using Java Path Finder. The model checker, working under the assumption of a nondeterministic environment, is able to efficiently verify critical properties of the design.",

author = "Andreas Griesmayer and Bloem, \{Roderick Paul\} and Martin Hautzendorfer and Franz Wotawa",

year = "2005",

doi = "10.1007/11504894\_108",

language = "English",

isbn = "3-540-26551-1",

series = "Lecture Notes in Computer Science ",

publisher = "Springer",

pages = "783--788",

editor = "Moonis Ali",

booktitle = "Innovations in Applied Artificial Intelligence",

address = "United States",

note = "18th International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems : IEA/AIE 2005, IEA/AIE 2005 ; Conference date: 22-06-2005 Through 24-06-2005",

}

TY - GEN

T1 - Formal verification of control software: A case study

AU - Griesmayer, Andreas

AU - Bloem, Roderick Paul

AU - Hautzendorfer, Martin

AU - Wotawa, Franz

PY - 2005

Y1 - 2005

N2 - We present a case study of formal verification of control logic for a robotic handling system. We have implemented a system in which properties can be specified in the source code, which is then automatically converted to Java and checked using Java Path Finder. The model checker, working under the assumption of a nondeterministic environment, is able to efficiently verify critical properties of the design.

AB - We present a case study of formal verification of control logic for a robotic handling system. We have implemented a system in which properties can be specified in the source code, which is then automatically converted to Java and checked using Java Path Finder. The model checker, working under the assumption of a nondeterministic environment, is able to efficiently verify critical properties of the design.

U2 - 10.1007/11504894_108

DO - 10.1007/11504894_108

M3 - Conference paper

SN - 3-540-26551-1

T3 - Lecture Notes in Computer Science

SP - 783

EP - 788

BT - Innovations in Applied Artificial Intelligence

A2 - Ali, Moonis

PB - Springer

CY - Berlin [u.a.]

T2 - 18th International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems

Y2 - 22 June 2005 through 24 June 2005

ER -

Formal verification of control software: A case study

Abstract

Publikationsreihe

Konferenz

Treatment code (Nähere Zuordnung)

Zugriff auf Dokument

Fingerprint

Projekte

EU - Prosyd - Property-Based System Design

Dieses zitieren