DocumentCode :
2318740
Title :
Derivation of formal representations from process-based specification and implementation models
Author :
Vercauteren, Steven ; Verkest, Diederik ; De Jong, Gjalt ; Lin, Bill
Author_Institution :
IMEC, Leuven, Belgium
fYear :
1997
fDate :
17-19 Sep 1997
Firstpage :
16
Lastpage :
23
Abstract :
We present a formal framework to verify timing properties of embedded systems. We propose a process calculus as an intermediate model to map between language level constructs of process based specification and implementation models, and Petri net operations. We present an elegant translation scheme to generate Petri nets starting from the intermediate process expressions. The approach has been applied to verify the freedom of deadlock in a QAM modem design, with promising results
Keywords :
Petri nets; formal specification; process algebra; program verification; real-time systems; Petri net operations; QAM modem design; deadlock; embedded systems; formal framework; formal representations; implementation models; intermediate model; intermediate process expressions; language level constructs; process based specification; process calculus; timing property verification; translation scheme; Assembly; Calculus; Embedded system; Formal verification; Hardware; Petri nets; Software tools; Specification languages; System recovery; Timing;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
System Synthesis, 1997. Proceedings., Tenth International Symposium on
Conference_Location :
Antwerp
ISSN :
1080-1820
Print_ISBN :
0-8186-7949-2
Type :
conf
DOI :
10.1109/ISSS.1997.621671
Filename :
621671
Link To Document :
بازگشت