Formalna weryfikacja automatycznego zrównoleglenia procesów

• Autorzy: Dziurzański P. , Karpicki M.

Warianty tytułu

EN

Formal verification of automatically parallelised processes

• Języki publikacji: PL

Abstrakty

PL

W artykule przedstawiono technikę formalnej weryfikacji systemów sprzętowo-programowych opisanych za pomocą języka opisu systemów SystemC. Formalnej weryfikacji dokonuje się z wykorzystaniem logiki temporalnej CTL i asercji. Przedstawiono formuły CTL dla systemu z jedną sekcją równoległą. Badania eksperymentalne wykazały liniowy wzrost liczby formuł i liniowy przyrost czasu działania programu automatycznie wstawiającego asercję, przez co prezentowane podejście nadaje się do zastosowań przemysłowych.

EN

In this paper, we present a formal verification technique of software/hardware systems given in the SystemC system description language. The verification is performed using temporal logic CTL and assertions. We enumerate the CTL formulas generated from a system with a single parallel section. Experimental results present a linear growth of a number of formulas and linear growth of the execution time of the developed tool that automatically inserts CTL assertions. Consequently, the proposed approach is suitable for industrial applications.

Słowa kluczowe

PL

formalna weryfikacja; logika temporalna CTL; asercja; równoleglizowanie; SystemC

EN

formal verification; parallelisation; assertion; SystemC

• Wydawca: Wydawnictwo PAK
• Czasopismo: Pomiary Automatyka Kontrola
• Rocznik: 2006
• Tom: R. 52, nr 11
• Strony: 35--38
• Opis fizyczny: Bibliogr, 9 poz., rys., tab., wzory

Twórcy

autor

Dziurzański P.

autor

Karpicki M.

• Wydział Informatyki, Politechnika Szczecińska,

Bibliografia

• [1] E. M. Clarke, E. A. Emerson, A. P. Sistla: Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), vol 8, no. 2, 1986, pp. 244-263.
• [2] J. Horgan, Assertion Based Verification: EDAWeekly Review, October 18-22, 2004.
• [3] N. Jayakumar, M. Purandare, F. Somenzi: Simulation coverage and generation for verification: Dos and don’ts of CTL state coverage estimation, Proceedings of the 40th Design Automation Conference (DAC’03), 2003, pp. 292-295.
• [4] K. Trifunović, P. Dziurzański, W. Bielecki: Sprzętowa implementacja pętli programowych, Pomiary, Automatyka, Kontrola, nr 7BIS, 2006, pp. 59-61.
• [5] M. Varea, B. M. Al-Hashimi, L. A. Cortes, P. Eles, Z. Peng: System design methods: analysis and verification: Symbolic model checking of Dual Transition Petri Nets, Proceedings of the Tenth International Symposium on Hardware/Software Codesign, 2002, pp. 43-48.
• [6] SystemC Version 2.0 User’s Guide, www.systemc.org , 2002.
• [7] C. Kern, M. R. Greenstreet: Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), vol. 4, no. 2, 1999, pp. 123-193.
• [8] M. Ben-Ari: Logika matematyczna w informatyce, WNT, Warszawa, 2005.
• [9] G. E. Fainekos, H. Kress-Gazit, G. J. Pappas: Temporal Logic Motion Planning for Mobile Robots, Proceedings of the 2005 IEEE International Conference on Robotics and Automation, Barcelona, Spain, April 2005.