Application of formal methods for hardware/software co-design of embedded systems

• Autorzy: Piotrowicz M.

Warianty tytułu

PL

Zastosowanie metod formalnych do wspomagania ko-projektowania poprawnych sterowników wbudowanych

• Języki publikacji: EN

Abstrakty

EN

In the paper a new co-verification technique for mixed hardware/software systems has been presented. The presented solution has hierarchical coloured Petri nets implemented for modelling the system and also the temporal logie for describing any technical requirement of the controller. The presented technique has been verified on a practical design of DC motor pulse controller. Such an attempt should shorten the design phase and could be a very efficient tool for co-verification of the integrated design methodology.

PL

W pracy przedstawiono nową metodologię projektowania mieszanych sterowników wbudowanych. Propozycja autora zakłada wykorzystanie hierarchicznych kolorowanych sieci Petriego do modelowania artefaktów projektowanego systemu oraz logii temporalnej do formułowania wymaganych własności. Metoda ta została zweryfikowana na praktycznym przykładzie projektu sterownika impulsowego silnika prądu stałego.

Słowa kluczowe

EN

co-design of embedded system; co-verification; mixed hardware/software systems; Petri nets; temporal logic; formal methods

PL

ko-projektowanie sterowników; ko-projektowanie; mieszane sterowniki wbudowane; sieci Petriego; logika temporalna; metody formalne

• Wydawca: Wydawnictwo Politechniki Łódzkiej
• Czasopismo: Zeszyty Naukowe. Elektryka / Politechnika Łódzka
• Rocznik: 2007
• Tom: z. 111
• Strony: 89--94
• Opis fizyczny: Bibliogr. 3 poz.

Twórcy

autor

Piotrowicz M.

• Technical University of Łódź, Department of Microelectronics and Computer Science

Bibliografia

• [1] Piotrowicz M.: Zastosowanie metod formalnych do wspomagania koprojektowania poprawnych sterowników wbudowanych, PhD thesis, Technical University of Łódź 2006.
• [2] Jensen K.: Coloured Petri Nets. Basic Concept, Analysis Methods and Practical Use, Vol.l, EATCS Monographs on Theoretical Computer Science, Springer-Verlag, Berlin 1992.
• [3] Jensen K., Christensen S., Kristensen L.M.: Design/CPN Occurrence Graph Manual, University of Aarhus, Denmark 1996.