Önellenőrzés és futásidejű verifikáció számítógépes programokban
Angol cím
Self-checking and run-time verification in computer programs
zsűri
Informatikai–Villamosmérnöki
Kutatóhely
Méréstechnika és Információs Rendszerek Tanszék (Budapesti Műszaki és Gazdaságtudományi Egyetem)
résztvevők
Csertán György Huszerl Gábor Pataricza András Pintér Gergely Varró Dániel
projekt kezdete
2004-01-01
projekt vége
2007-12-31
aktuális összeg (MFt)
4.352
FTE (kutatóév egyenérték)
0.00
állapot
lezárult projekt
Zárójelentés
kutatási eredmények (magyarul)
A kutatás eredménye egy olyan, futásidejű hibadetektálásra alkalmas módszerkészlet kidolgozása számítógépes programokhoz, amely formálisan megalapozott és illeszkedik a modell alapú tervezési folyamathoz. A futásidejű verifikáció matematikai alapja egy általunk definiált, UML állapottérképekhez illesztett temporális logikai nyelv (SC-LTL) valamint az ehhez kidolgozott gyors és kis erőforrásigényű ellenőrzési algoritmus. Az ellenőrzést megvalósító forráskód részletek (assertions) generálására automatikus kódgenerátort fejlesztettünk.
A módszerkészlet alapján a futásidejű verifikáció két szinten végezhető el: (1) A fejlesztés korai fázisaiban (a követelményanalízis után) a tervező a program biztonságos működéséhez tartozó követelményeket formalizálja az SC-LTL temporális logika segítségével. Ezeket futásidőben a programba illesztett kódrészletek segítségével ellenőrizzük. Így a későbbi fejlesztési fázisokban előforduló tervezési hibák következményei is kimutathatók. (2) A fejlesztés előrehaladtával rendelkezésre álló részletes viselkedési modell mint referencia alapján történik a program állapot- és akciószekvenciáinak teljes ellenőrzése, a modellből szintén automatikusan generált, futásidejű monitorozást biztosító úgynevezett watchdog kód segítségével. Ennek célja elsősorban az implementációs hibák és a működési hibák (tranziens hardver hibák) felderítése. A hibadetektálás módszerkészletét kiegészítettük a hibakezelés modellezésére és verifikációjára szolgáló eljárásokkal.
kutatási eredmények (angolul)
The main result of the research is the elaboration of a set of methods that can be applied for the run-time verification of computer programs. These methods are formally proven and fit well to the model based software development process. The mathematical basis of run-time verification is our temporal logic language (SC-LTL) that is based on UML statechart diagrams, and the corresponding fast and low resource-demanding checker algorithm. To derive the assertions (i.e., the program code snippets that implement the checking), we have developed an automatic source code generator.
On the basis of this set of methods, run-time checking of program execution is supported at two levels: (1) In the early phases of development the designer can formalize the program safety and liveness requirements using SC-LTL. These requirements are checked in run-time by the automatically generated assertions. This way design errors introduced in later design phases can also be detected. (2) The full checking of the state- and action sequences of program execution is based on a detailed design model constructed in the last development phases. The run-time monitoring is performed by a so-called watchdog code that is generated from the fully elaborated statechart model automatically. This is able to detect both implementation and operational errors. To complete the error detection framework, we proposed a statechart based method for the modeling and verification of run-time exception handling.
Pintér G; Majzik I: High-Level Supervision of Program Execution Based on Formal Specification, In: Int. Conference on Dependable Systems and Networks - Workshop on Architecting Dependable Systems (WADS), Florence: 2004. pp. 292-296, 2004
Pintér G; Majzik I: Impact of Statechart Implementation Techniques on the Effectiveness of Fault Detection Mechanisms, In: 30th EUROMICRO Conference, Component Based Software Engineering Track, Rennes: 2004. pp. 136-143, 2004
Pintér G; Majzik I: Modeling and Analysis of Exception Handling by Unsing UML Statecharts, In: International Workshop on Scientific Engineering of Distributed Java Applications (FIDJI), Luxembourg-Kirchberg: 2004. pp. 69-78, 2004
Pintér G: Abstract Model-Based Checkpoint and Recovery, In: The Fourth Conference of PhD Students in Computer Science (CSCS), Szeged: 2004., 2004
Micskei Z: Automatikus tesztgenerálás modell ellenőrzővel, In: Fiatal Műszakiak X. Tudományos Ülésszaka, Kolozsvár: 2005, pp. 47-50, ISBN 973-8231-44-2, 2005
Pintér G; Majzik I: Runtime Verification of Statechart Implementations, In: de Lemos R; Gacek C; Romanovsky A (eds.), Architecting Dependable Systems III, Berlin: Springer Verlag, 2005, pp 148-172, ISBN 3-540-28968-5, 2005
Pintér G; Majzik I: Automatic Generation of Executable Assertions for Runtime Checking Temporal Requirements, In: 9th IEEE Int. Symposium on High Assurance Systems Engineering (HASE ’05), Heidelberg: 2005, pp. 111-120, IEEE CS, ISBN 0-7695-2377-3, 2005
Pintér G; Majzik I: Modeling and Analysis of Exception Handling by Using UML Statecharts, In: Guelfi N; Reggio G; Romanovsky A (eds.), Scientific Engineering of Distributed Java Applications, Berlin: Springer Verlag, 2005, pp. 58-67, ISBN 3-540-2505, 2005
Pintér G: Futási idejű ellenőrzés absztrakt modellek alapján, In: Fiatal Műszakiak X. Tudományos Ülésszaka, Kolozsvár: 2005, pp. 138-140, ISBN 973-8231-44-2, 2005
Pintér G; Majzik I: Error Detection in Control Flow of Event-Driven State Based Applications, In: P. Pelliccione, H. Muccini, N. Guelfi, A. Romanovsky (eds.), Software Engineering and Fault Tolerance, World Scientific Publishing Co. Pte. Ltd, accepted, 2007
Micskei Z; Majzik I: Model-Based Automatic Test Generation for Event-Driven Embedded Systems Using Model Checkers, In: International Conference on Dependability of Computer Systems (DepCoS – RELCOMEX), Wroclaw, Poland: 2006IEEE Computer Society, pp 191-198., 2006
Pintér G; Majzik I: Formal Operational Semantics for UML 2.0 Statecharts, In: Technical Report, Budapest University of Technology and Economics, 150 pages, 2006
