Alvis is a modelling language defined for the design and a formal verification of embedded systems. An Alvis model is a system of agents that usually run concurrently, communicate one with another, compete for shared resources etc. Due to the fact that an embedded system usually collects inputs that come from its environment and provides outputs that go to the environment it is necessary to provide a mechanism to describe such a communication. In contrast to another formal languages used to model embedded systems it is not necessary, using Alvis, to design such an environment as a part of a model. The paper deals with the problem of modelling a communication with an embedded system environment with Alvis.
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
The paper presents a formal description of a subset of the Alvis language designed for the modelling and formal verification of concurrent systems. Alvis combines possibilities of a formal models verification with flexibility and simplicity of practical programming languages. Alvis provides a graphical modelling of interconnections among agents and a high level programming language used for the description of agents behaviour. Its semantic depends on the so-called system layer. The most universal system layer α0, described in the paper, makes Alvis similar to other formal languages like Petri nets, process algebras, time automata, etc.
Alvis jest językiem modelowania, rozwijanym głównie z myślą o projektowaniu i weryfikacji systemów wbudowanych. Wywodzi się on z algebr procesów CCS i XCCS, ale w języku tym równania algebraiczne zostały zastąpione przez język programowania wysokiego poziomu oparty na języku Haskell. W przeciwieństwie do algebr procesów, które umożliwiają wyłącznie tekstowy opis systemów wbudowanych, w języku Alvis struktura projektowanego systemu, z punktu widzenia przepływu danych i sterowania, przedstawiana jest graficznie za pomocą diagramów komunikacji. Poniższy artykuł zawiera wprowadzenie do języka Alvis zilustrowane modelem sterownika dla robota mobilnego Hexor II.
EN
Alvis is a novel modelling language defined especially for the embedded systems design and verification. The language has its origin in CCS and XCCS process algebras, but algebraic equations have been replaced with a Haskell based high level programming language. Moreover, Alvis provides communication diagrams for the visual modelling of an embedded system structure, especially from the control and data-flow point of view. This paper presents an introduction to Alvis based on a model of a controller for the Hexor II mobile robot.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.