Model Checking Embedded Systems with PROMELA

descriptionPublicationkeyboard_double_arrow_right Article , Conference object 19 Apr 2005 Portugal Publisher:IEEEJournal:12th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems (ECBS'05)

Authors: Ribeiro, Óscar R.; Fernandes, João M.; Pinto, Luís F.;

doi: 10.1109/ecbs.2005.53

handle: 1822/905

Model Checking Embedded Systems with PROMELA

- Summary
- Metrics

Abstract

The design process for embedded systems can benefit from the usage of formal methods, if some properties of the systems are checked, before design and implementation decisions are accomplished. This paper presents a model checking approach using the Spin tool, to verify some important properties of embedded systems, namely liveness, deadlock-freedom, and structural conflicts among transitions. The systems are modelled with a variant of Petri nets, called SIPN (synchronous and interpreted Petri nets), and this paper discusses how SIPN models should be specified with the PROMELA language (input format for the Spin model checker). The approach is exemplified with a case study.

Country

Portugal

Related Organizations

University of Minho
Portugal

Impact byBIP!

	selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	8
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Top 10%
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average