Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Rialto to B: An Exercise in Fo...

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

Dag Björklund, Johan Lilius, Rialto to B: An Exercise in Formal Development of a Language for Multiple Models of Computation. In: Fourth International Conference on Application of Concurrency to System Design, 125-134, IEEE Computer Society, 2004.

Abstract:

Rialto is a textual language for modeling heterogeneous systems, where different computational models are represented by scheduling policies that manage concurrent activities in the system. Rialto has a formal semantics defined using structured operational rules, which allows for the application of formal verification techniques to programs in the language. We show that the B method is suitable for this purpose. We present a novel approach for translating the language into B, where we have specified the actual Rialto semantics as a program interpreter in B. Rialto programs can automatically be translated into B specifications and we can use this interpreter to animate and validate them.

BibTeX entry:

@INPROCEEDINGS{inpBjLi04a,
  title = {Rialto to B: An Exercise in Formal Development of a Language for Multiple Models of Computation},
  booktitle = {Fourth International Conference on Application of Concurrency to System Design},
  author = {Björklund, Dag and Lilius, Johan},
  publisher = {IEEE Computer Society},
  pages = {125-134},
  year = {2004},
}

Belongs to TUCS Research Unit(s): Embedded Systems Laboratory (ESLAB)

Edit publication