Formal Verification of Embedded Systems Using the Alvis Approach

Leszek Kotulski; Marcin Szpyrka

doi:10.4028/www.scientific.net/KEM.486.209

Paper Titles

The Design and Optimization of the Diversion-Type Tidal Current Turbine
p.193

Ecological Impact Assessment and Eco-Design of Industrial Gearboxes
p.197

CAD/CAM for Five-Axis Printing Machine
p.201

Kinematic Calibration of PHANTOM Premium 1.5/6DOF Haptic Device
p.205

Formal Verification of Embedded Systems Using the Alvis Approach
p.209

Prediction of Wrinkling and Bursting in Hydroforming of Tubes in Box-Shaped Die Using FEM
p.213

Multi-Agent System for Distributed Adaptive Design
p.217

Modal Parameters Identification Accuracy with a Short Time Parametric Algorithm
p.221

Analysis of Feature and Welding Consideration for Metal Bellows
p.225

HomeKey Engineering MaterialsKey Engineering Materials Vol. 486Formal Verification of Embedded Systems Using the...

Formal Verification of Embedded Systems Using the Alvis Approach

Abstract:

Embedded systems are usually characterized by time-critical reactions and increased complexity. Because it is usually impossible to correct a system bug by simply uploading of a new version of a system software or firmware, a system behavior should be verified in a formal manner. The Alvis approach presented in this paper is able to verify the system behavior, by specifying the border between a developed embedded system and its environment. The means to move the border is then proposed, which allows the designer to create a formal representation for selected parts of a model only.

You might also be interested in these eBooks

View Preview

Info:

Periodical:

Key Engineering Materials (Volume 486)

Pages:

209-212

DOI:

https://doi.org/10.4028/www.scientific.net/KEM.486.209

Citation:

Cite this paper

Online since:

July 2011

Authors:

Leszek Kotulski, Marcin Szpyrka

Keywords:

Embedded System, Formal Verification, Graphical Modelling

Export:

RIS, BibTeX

Price:

Permissions CCC:

Request Permissions

Permissions PLS:

Request Permissions

Сopyright:

Citation:

References

[1] M. Szpyrka, P. Matyasik, R. Mrówka: Alvis - modelling language for concurrent systems, in: Intelligent Decision Systems in Large-Scale Distributed Environments, edited by P. Bouvry, H. Gonzalez-Velez, J. Kołodziej, Studies in Computational Intelligence,chapter 15, Springer (2011).

DOI: 10.1007/978-3-642-21271-0_15

Google Scholar

[2] R. Milner: Communication and Concurrency, Prentice-Hall (1989).

Google Scholar

[3] K. Balicki, M. Szpyrka: Formal definition of XCCS modelling language, Fundamenta Informaticae, vol. 93, no. 1-3, pp.1-15 (2009).

DOI: 10.3233/fi-2009-0084

Google Scholar

[4] M. Szpyrka: On-line Alvis Manual, http://fm.ia.agh.edu.pl/alvis:manual (2011).

Google Scholar

[5] M. Flasinski: Inference of parsable graph grammars for syntactic pattern recognition. Fundaments Informaticae, vol. 80, pp.379-412 (2007)

Google Scholar

[6] H. Garavel, F. Lang, R. Mateescu, W. Serwe: CADP 2006:A Toolbox for the Construction and Analysis of Distributed Processes, LNCS, vol. 4590, Springer, pp.158-163 (2007).

DOI: 10.1007/978-3-540-73368-3_18

Google Scholar