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

• Autorzy: Björklund. D. , Lilius J.
• Języki publikacji: EN

Abstrakty

EN

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.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2006
• Tom: Vol. 70, nr 1,2
• Strony: 1--20
• Opis fizyczny: bibliogr. 24 poz.

Twórcy

autor

Björklund. D.

autor

Lilius J.

• Turku Centre for Computer Science TUCS, Department of Computer Science, Abo Akademii University, Lemminkäisenkatu 14A, FIN-20520 Turku, Finland,

Bibliografia

• [1] Météor, Available at http://www.siemens-ts.com/pagesUS/produits/Meteor.htm
• [2] Abrial, J.-R.: The B-Method for Large Software Specification, Design and Coding, VDM'91 Formal Software Development Methods, 2, Springer-Verlag, october 1991.
• [3] Abrial, J.-R., Mussat, L.: Introducing Dynamic Constraints in B, Proceedings of the 2nd International B Conference, B'98, 1998.
• [4] Atelier B, by Clearsy system engineering: Internet: http://www.atelrierb.societe.com
• [5] The B Toolkit by B-Core(UK) Ltd: Internet http:://www.b-core.com/btoolkit.html.
• [6] Björklund, D.: Efficient Code Synthesis from Synchronous Dataflow Graphs, Proceedings of the Second ACM& IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'2004), 2004.
• [7] Björklund, D., Lilius, J.: From UML Behavioral Models to Efficient Synthesizable VHDL, Proceedings of the 20th IEEE Norchip Conference, November 2002.
• [8] Björklund, D., Lilius, J.: A Language for Multiple Models of Computation, Symposium on Hardware/ Software Codesign 2002, ACM Press, May 2002.
• [9] Björklund, D., Lilius, J.: A Unified Approach to Code Generation from Behavioral Diagrams, Forum on specification and design languages (FDL'03), 2003.
• [10] Björklund, D., Lilius, J., Porres, I.: Towards Efficient Code Synthesis from Statecharts, pUML Workshop at UML2001 (A. Evans, R. France, A. Moreira, B. Rumpe, Eds.), October 2001.
• [11] Butler, M., Snook, C.: UML-B - Formal modelling with UML, http://www.ecs.soton.ac.uk/~cfs/umbl.html
• [12] The HOL System: Internet: http://www.cl.cam.ac.uk/Research/HVG/HOL
• [13] Holzmann, G.: The model checker SPIN, IEEE Transactions on Software Engineering, 23(5), May 1997.
• [14] The Isabelle Theorem Prover: http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
• [15] Kelsey, R., Clinger, W., (eds.), J. R.: Revised_ Report on the Algorithmic Language Scheme, Higher-Order and Symbolic Computation, 11(1), 1998.
• [16] Lanet, J.-L., Lartigue, P.: The Use of Formal Methods for Smart Cards, a Comparison between B ans SDL to Model the T=1 Protocol, Available at http://www.gemplus.com/smart/r_d/publications/art7/htm further information about the use use of the B-Method at GemPlus is available at http://www.gemplus.com/smart/r_d/trends/system_model/b-method/.
• [17] Ledang, H., Souquiéres, J.: Contributions forModelling UML State-Charts in B, Integrated FormalMethods. 3rd Internatinal Conference, IFM 2002, Turku Finland (M. Butler, L. Petre, K. Sere, Eds.), Springer-Verlag, May 2002.
• [18] Lee, E. A.: Embedded Software, Advances in Computers (M. Zelkowitz, Ed.), 56, Academic Press, London, 2002.
• [19] OMG: OMG Unified Modeling Language Specification, Version 1.5, March 2003, available at www.omg.org.
• [20] OMG: OMG XML Metadata Interchange (XMI) Specification, OMG Document formal/00-11-02.Available at www.omg.org.
• [21] Plotkin, G.: A Structural Approach to Operational Semantics, DAIMI FN 19, Computer Science Dept., Aarhus University, April 1981.
• [22] Porres, I.: A Toolkit for Manipulating UML Models, Technical Report 441, Turku Centre for Computer Science, 2002.
• [23] Sekerinski, E., Zurob, R.: iState: A Statechart Translator, UML2001 - The Unified Modeling Language. Modeling Languages, Concepts, and Tools (M. Gogolla, C. Kobryn, Eds.), Springer-Verlag, October 2001.
• [24] Sekerinski, E., Zurob, R.: Translating Statecharts to B, Integrated Formal Methods. 3rd Internatinal Conference, IFM 2002, Turku Finland (M. Butler, L. Petre, K. Sere, Eds.), Springer-Verlag, May 2002.