Rialto to B: An Exercise in Formal Development of a Language for Multiple Models of Computation

Issue title: APPLICATION OF CONCURRENCY TO SYSTEM DESIGN (ACSD'04)

Article type: Research Article

Authors: Björklund, Dag | Lilius, Johan

Affiliations: Turku Centre for Computer Science (TUCS), Department of Computer Science, Åbo Akademi University, Lemminkäisenkatu 14 A, FIN-20520, Turku, Finland. E-mail: dbjorklu,[email protected]

Abstract: The B method is one of the few formal methods with commerciallly available tool support. It has been succesfully applied in the development of several industrial applications. In this paper we present an application of the B-Method to a new domain, namely language development. We have developed an approach for translating a language with a structural operational semantics into B specifications. The language semantics is specified in separate B machines, that act as an interpreter for programs in the language. The programs, represented as abstract syntax trees, can then automatically be translated into B specifications. We have used the approach in the context of Rialto, a language for multiple models of computation. We show how Rialto programs are translated into B machines, and how the different scheduling policies that are used to interpret concurrency can be also be represented as B machines. We also discuss some shortcomings of the approach and the B-Tools that we have available.

Journal: Fundamenta Informaticae, vol. 70, no. 1-2, pp. 1-20, 2006