Geodesic
Distributed embedded control systems design with verification support
Modelirovanie i analiz informacionnyh sistem, Tome 17 (2010) no. 4, pp. 125-136.

Voir la notice de l'article provenant de la source Math-Net.Ru

We consider a problem of integrating a formal method of verification (model checking) into the process of designing complex distributed software systems to improve the quality of software. We use an approach based on the Model-Driven Engineering. It allows us to structure the design process by selecting and verifying a system core, consisting of independent subsystems and being responsible for logical management of the entire system as a whole. The proposed method was tested on a real control system of vessel power supply.
Keywords: Model-Driven Engineering, model checking, UML, LTL
Mots-clés : Promela. 
@article{MAIS_2010_17_4_a12,
     author = {I. V. Shoshmina},
     title = {Distributed embedded control systems design  with verification support},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {125--136},
     publisher = {mathdoc},
     volume = {17},
     number = {4},
     year = {2010},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a12/}
}
TY  - JOUR
AU  - I. V. Shoshmina
TI  - Distributed embedded control systems design  with verification support
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2010
SP  - 125
EP  - 136
VL  - 17
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a12/
LA  - ru
ID  - MAIS_2010_17_4_a12
ER  - 
%0 Journal Article
%A I. V. Shoshmina
%T Distributed embedded control systems design  with verification support
%J Modelirovanie i analiz informacionnyh sistem
%D 2010
%P 125-136
%V 17
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a12/
%G ru
%F MAIS_2010_17_4_a12
I. V. Shoshmina. Distributed embedded control systems design  with verification support. Modelirovanie i analiz informacionnyh sistem, Tome 17 (2010) no. 4, pp. 125-136. http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a12/

[1] W. W. Royce, “Managing the Development of Large Software Systems”, Proceedings of the 9th International Software Engineering Conference, Computer Society Press, 1987, 328–338

[2] Model Driven Architecture (MDA), ormsc/2001-07-01: OMG, 2001

[3] Yu. G. Karpov, Model Checking. Verifikatsiya parallelnykh i raspredelennykh programmnykh sistem, BKhV-Peterburg, SPb, 2010

[4] P. Kruchten, The Rational Unified Process: An Introduction, Addison-Wesley Longman Publishing Co., Inc., 2003

[5] B. Pages, BoUML user manual, , 2010 http:/bouml.free.fr

[6] G. Holzmann, Spin Model Checker, The Primer and Reference Manual, Addison Wesley, 2003

[7] A. N. Valikov, Tekhnologiya XSLT, BKhV-Peterburg, SPb., 2002

[8] OMG Unified Modeling Language (OMG UML), Superstructure, v2.1.2. Object Management Group (OMG), , 2007 http://www.omg.org/spec/UML/2.1.2/Superstructure/PDF

[9] A. A. Shalyto, N. I. Tukkel, “Proektirovanie programmnogo obespecheniya sistemy upravleniya dizel-generatorami na osnove avtomatnogo podkhoda”, Sistemy upravleniya i obrabotki informatsii, 5, FGUP «NPO «Avrora», SPb., 2003, 62–82 | MR

[10] A. Ya. Kalinov, A. S. Kosachev, M. A. Posypkin, A. A. Sokolov, “Avtomaticheskaya generatsiya testov dlya graficheskogo polzovatelskogo interfeisa po UML-diagrammam deistvii”, Trudy instituta sistemnogo programmirovaniya RAN, ch. 1, 8, M., 2004, 99–117