Alvis Modelling Language for Embedded Systems

Organisation:	AGH University of Science and Technology (Krakow, POLAND)
Functionality:	Design and verification of embedded systems.
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Period:	2010-2012
Description:	The Alvis modelling language has been designed specifically for the design and verification of embedded systems. It takes its roots in the CSS and XCCS process algebras, but with a Haskell-based high-level programming language syntax replacing algebraic equations. It also contains a graphical layer that is used to define communications between the various components in a model. Alvis is intended to be easier for systems designers to use than classical formal methods. The XCCS algebraic layer has been replaced with a completely new Alvis code layer. Instead of algebraic equations, Alvis uses a high level programming language based on the Haskell syntax. Moreover, Haskell is used to define data types for parameters and to define functions for data manipulation. An Alvis definition of a system consists of the specifications of the system components (known as agents), written in the Alvis Behavior Description Language, communication diagrams that define the conections between agents, and a meta-data layer that is generated automatically and is used to generate the Labelled Transition System (LTS) to be used to verify the model. The LTS is encoded in BCG format, and the EVALUATOR model checker of CADP is used to check whether the LTS satifies its requirements. The Alvis language and tool is illustrated by analyzing the model of the ATmega128 microcontroller of the Hexor II autonomous 6-legged mobile robot. The tasks of that chip are as follows: scanning sensors (sonar, tentacles, infrared), generating signals for servos (PWM), and executing the movement algorithm.
Conclusions:	Defined for embedded systems design, Alvis seems to be more accessible for engineers than classical formal methods, but still preserves a possibility of formal verification by means of a connection to the CADP toolbox. The implementation of the embedded control system for the Hexor robot in Alvis demonstrates the success of this approach to designing safe embedded systems.
Publications:	[Szpyrka-Matyasik-Mrowka-10] Marcin Szpyrka, Piotr Matyasik, and Rafal Mrówka. "Alvis approach to Hexor robot controller development". Proceedings of the 17th International Conference on Mixed Design of Integrated Circuits and Systems (MIXDES) (Wroclaw, Poland), 595-600, IEEE, June 2010. Available on line at: http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5551327 or from the CADP Web site in PDF or PostScript [Szpyrka-Matyasik-Mrowka-11] Marcin Szpyrka, Piotr Matyasik, and Rafal Mrówka. "Alvis - Modelling Language for Concurrent Systems". Intelligent Decision Systems in Large-Scale Distributed Environments, pages 315-341, Springer Verlag, 2011. Available on line at: http://www.springerlink.com/content/e4525kq11m270503 [Szpyrka-Nalepa-Ligeza-Kluza-11] Marcin Szpyrka, Grzegorz Nalepa, Antoni Ligeza, and Krzysztof Kluza. "Proposal of Formal Verification of Selected BPMN Models with Alvis Modeling Language". Proceedings of the 5th International Symposium on Intelligent Distributed Computing IDC'2011 (Delft, The Netherlands), Studies in Computational Intelligence 382, October 2011. Available on line at: http://link.springer.com/chapter/10.1007/978-3-642-24013-3_26 [Szpyrka-Matyasik-Mrowka-Kotulski-12] Marcin Szpyrka, Piotr Matyasik, Rafal Mrówka, and Leszek Kotulski. "Communication with Environment in Alvis Models". International Journal of Electronics and Telecommunications 58(3):247-254, 2012. Available on line at: http://www.degruyter.com/view/j/eletel.2012.58.issue-3/v10177-012-0034-2/v10177-012-0034-2.xml or from the CADP Web site in PDF or PostScript [Szpyrka-Matyasik-Wypych-13] Marcin Szpyrka, Piotr Matyasik, and Michal Wypych. "Generation of Labelled Transition Systems for Alvis Models Using Haskell Model Representation". Proceedings of the 22nd International Workshop on Concurrency, Specification and Programming CS&P'2013 (Warsaw, Poland), pp. 409-420, September 2013. Available on line at: http://ceur-ws.org/Vol-1032/paper-36.pdf or from the CADP Web site in PDF or PostScript [Matyasik-14] Piotr Matyasik. "Alvis Virtual Machine". Proceedings of the 2014 Federated Conference on Computer Science and Information Systems FedCSIS'14 (Warsaw, Poland), pp. 1639-1645, IEEE, September 2014. Available on line at: http://fedcsis.org/proceedings/2014/pliks/267.pdf or from the CADP Web site in PDF or PostScript [Szpyrka-Matyasik-Biernacki-et-al-16] Marcin Szpyrka, Piotr Matyasik, Jerzy Biernacki, Agnieszka Biernacka, Michal Wypych, and Leszek Kotulski. "Hierarchical Communication Diagrams". Computing and Informatics 35:55-83, 2016. Available on line at: http://www.cai.sk/ojs/index.php/cai/article/viewArticle/2961 or from the CADP Web site in PDF or PostScript [Szpyrka-Nalepa-Kluza-17] Marcin Szpyrka, Grzegorz J. Nalepa, and Krzysztof Kluza. "From Process Models to Concurrent Systems in Alvis Language". Informatica 28(3):525-545, 2017. Available on line at: https://www.mii.lt/informatica/pdf/INFO1153.pdf or from the CADP Web site in PDF or PostScript [Szpyrka-Podolski-Wypych-18] Marcin Szpyrka, Lukasz Podolski, and Michal Wypych. "Modelling and Verification of Real-Time Systems with Alvis". In "Towards a Synergistic Combination of Research and Practice in Software Engineering", pages 165-178, Springer Verlag, 2018. Available on line at: https://www.mii.lt/informatica/pdf/INFO1153.pdf or from the CADP Web site in PDF or PostScript [Wypych-21] Michal Wypych. "Methods of Generation of Transition Systems for ALVIS Language". PhD Thesis, University of Science and Technology in Krakow, Poland, 2021. Available on line at: https://doktoraty.iet.agh.edu.pl/_media/2022:micwypych:michal_wypych_metody_generowania_etykietowanych_systemow_przejsc_dla_jezyka_alvis.pdf or from the CADP Web site in PDF or PostScript
Contact:	Marcin Szpyrka Department of Automatics AGH University of Science and Technology Krakow Poland Email: mszpyrka@agh.edu.pl
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page