An algebraic approach to correctness verification of graphical software specifications is presented. LACATRE graphical language based on multitasking and providing real-time functions is considered as a specification tool. The verification process is distributed into four stages. The two initial ones are related to a translation of LACATRE specification into lower description level (Communicating Real-Time State Machines). ; The third stage deals with a generation of the process in the form of a graph of states and automatic relative correctness verification. The fourth stage is related to correctness verification for user-defined criteria. The proposed verification method examines the relative correctness concept introduced in former papers.
Zielona Góra: Uniwersytet Zielonogórski
Korbicz, Józef - red. ; Uciński, Dariusz - red.
AMCS, volume 4, number 4 (1994)
Biblioteka Uniwersytetu Zielonogórskiego
Jul 29, 2020
Jul 29, 2020
5
https://www.zbc.uz.zgora.pl/publication/63953
Edition name | Date |
---|---|
Towards automatic correctness verification of real-time programs | Jul 29, 2020 |
Szmuc, Tomasz Korbicz, Józef - red. Uciński, Dariusz - red.
Xu, Li Saito, Osami Abe, Kenichi Kaczorek, Tadeusz - ed.
Trzaska, Zdzisław W. Kaczorek, Tadeusz - ed.
Rocha, Paula Wood, Jeffrey Kaczorek, Tadeusz - ed.
Krasoń, Ewa Kaczorek, Tadeusz - ed.
Kaczorek, Tadeusz Giang, Nguyen Bang Kaczorek, Tadeusz - ed.
Kaczorek, Tadeusz Kaczorek, Tadeusz - ed.