CoreASM: An Extensible ASM Execution Engine

• Autorzy: Farahbod R. , Gervasi V. , Glässer U.
• Języki publikacji: EN

Abstrakty

EN

In this paper we introduce a new research effort in making abstract state machines (ASMs) executable. The aim is to specify and implement an execution engine for a language that is as close as possible to the mathematical definition of pure ASMs. The paper presents the general architecture of the engine, together with a high-level description of the extensibility mechanisms that are used by the engine to accommodate arbitrary backgrounds, scheduling policies, and new rule forms.

Słowa kluczowe

EN

coreASM; abstract state machines; specification languages; executable specification

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 77, nr 1,2
• Strony: 71--103
• Opis fizyczny: bibliogr. 51 poz., wykr.

Twórcy

autor

Farahbod R.

autor

Gervasi V.

autor

Glässer U.

• School of Computing Science, Simon Fraser University, Burnaby, B.C., Canada,

Bibliografia

• [1] Anlauff, M.: XASM - An Extensible, Component-Based Abstract State Machines Language, Abstract State Machines: Theory and Applications (Y. Gurevich and P. Kutter and M. Odersky and L. Thiele, Ed.), 1912, Springer-Verlag, 2000.
• [2] Anlauff, M., Kutter, P.: eXtensible Abstract State Machines, XASM open source project: http://www. xasm.org. R. Farahbod et al. /CoreASM: An Extensible ASM Execution Engine 101
• [3] Beckert, B., Posegga, J.: leanEA: A Lean Evolving Algebra Compiler, Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL'95) (H. K. Büning, Ed.), 1092, Springer, 1996.
• [4] Beierle, C., Börger, E., Durdanovic, I., Glässer, U., Riccobene, E.: Refining Abstract Machine Specifications of the Steam Boiler Control to Well Documented Executable Code, in: Formal Methods for Industrial Applications. Specifying and Programming the Steam-Boiler Control (J.-R. Abrial, E. Börger, H. Langmaack, Eds.), number 1165 in LNCS, Springer, 1996, 62-78.
• [5] Blass, A., Gurevich, Y.: Abstract State Machines Capture Parallel Algorithms, ACM Transactions on Computation Logic, 4(4), 2003, 578-651.
• [6] Börger, E.: A Logical Operational Semantics for Full Prolog. Part I: Selection Core and Control, CSL'89. 3rd Workshop on Computer Science Logic (E. Börger, H. Kleine Büning, M. M. Richter, W. Schönfeld, Eds.), 440, Springer, 1990.
• [7] Börger, E.: A Logical Operational Semantics of Full Prolog. Part II: Built-in Predicates for Database Manipulation, in: Mathematical Foundations of Computer Science (B. Rovan, Ed.), vol. 452 of LNCS, Springer, 1990, 1-14.
• [8] Börger, E.: The Origins and the Development of the ASM Method for High Level System Design and Analysis, Journal of Universal Computer Science, 8(1), 2002, 2-74.
• [9] Börger, E.: The ASM Ground Model Method as a Foundation for Requirements Engineering, Verification: Theory and Practice, 2003.
• [10] Börger, E.: The ASM Refinement Method, Formal Aspects of Computing, 2003, 237-257.
• [11] Börger, E., Fruja, N. G., Gervasi, V., Stärk, R. F.: A high-level modular definition of the semantics of C#, Theoretical Computer Science, 336(2/3), May 2005, 235-284.
• [12] Börger, E., Glässer, U., Müller, W.: The Semantics of Behavioral VHDL'93 Descriptions, EURO-DAC'94. European Design Automation Conference with EURO-VHDL'94, IEEE CS Press, Los Alamitos, California, 1994.
• [13] Börger, E., Glässer, U., Müller, W.: Formal Definition of an Abstract VHDL'93 Simulator by EA-Machines, in: Formal Semantics for VHDL (C. Delgado Kloos, P. T. Breuer, Eds.), Kluwer Academic Publishers, 1995, 107-139.
• [14] Börger, E., Päppinghaus, P., Schmid, J.: Report on a Practical Application of ASMs in Software Design, Abstract State Machines: Theory and Applications (Y. Gurevich and P. Kutter and M. Odersky and L. Thiele, Ed.), 1912, Springer-Verlag, 2000.
• [15] Börger, E., Riccobene, E., Schmid, J.: Capturing Requirements by Abstract State Machines: The Light Control Case Study, Journal of Universal Computer Science, 6(7), 2000, 597-620.
• [16] Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis, Springer-Verlag, 2003.
• [17] Castillo, G. D., Glässer, U.: Simulation and Validation of High-level Abstract State Machine Specifications, Modelling and Simulation: A Tool for the Next Millenium - Proc. of the 13th European Simulation Multiconference (H. Szczerbicka, Ed.), 2, June 1999.
• [18] Del Castillo, G.: Towards Comprehensive Tool Support for Abstract State Machines, Applied Formal Methods - FM-Trends 98 (D. Hutter, W. Stephan, P. Traverso, M. Ullmann, Eds.), 1641, Springer-Verlag, 1999.
• [19] Del Castillo, G., Durdanović, I., Glässer, U.: An Evolving Algebra Abstract Machine, Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL'95) (H. K. Büning, Ed.), 1092, Springer, 1996.
• [20] Del Castillo, G., Glässer, U.: Computer-Aided Analysis and Validation of Heterogeneous System Specifications, Computer Aided Systems Theory: Proceedings of the 7th International Workshop on Computer Aided Systems Theory (EUROCAST'99) (F. Pichler, R. Moreno-Diaz, P. Kopacek, Eds.), 1798, Springer, 2000.
• [21] Del Castillo, G., Winter, K.: Model Checking Support for the ASM High-Level Language, Proceedings of the 6th International Conference TACAS 2000 (S. Graf, M. Schwartzbach, Eds.), 1785, Springer-Verlag, 2000.
• [22] Diesen, D.: Specifying Algorithms Using Evolving Algebra. Implementation of Functional Programming Languages, Dr. scient. degree thesis, Dept. of Informatics, University of Oslo, Norway, March 1995.
• [23] E. Börger and W. Schulte: A Practical Method for Specification and Analysis of Exception Handling: A Java/JVM Case Study, IEEE Transactions on Software Engineering, 26(10), October 2000, 872-887.
• [24] Eclipse Foundation: Eclipse.org web site, Last visited May 2005, http://www.eclipse.org/.
• [25] Eschbach, R., Glässer, U., Gotzhein, R., Prinz, A.: On the Formal Semantics of SDL-2000: A Compilation Approach Based on an Abstract SDL Machine, Abstract State Machines: Theory and Applications (Y.Gurevich and P. Kutter and M. Odersky and L. Thiele, Ed.), 1912, Springer-Verlag, 2000.
• [26] Farahbod, R., Gervasi, V., Glässer, U.: Design and Specification of the CoreASMExecution Engine, Technical Report SFU-CMPT-TR-2005-02, Simon Fraser University, February 2005.
• [27] Farahbod, R., Gervasi, V., Glässer, U.: Design and Specification of the CoreASMExecution Engine, Technical report, Simon Fraser University, To be published in October 2005, Revised version of SFU-CMPT-TR-2005-02, February 2005.
• [28] Farahbod, R., Glässer, U., Vajihollahi, M.: Specification and Validation of the Business Process Execution Language for Web Services, Abstract State Machines 2004. Advances In Theory And Practice: 11th International Workshop (ASM 2004) (W. Zimmermann, B. Thalheim, Eds.), Springer-Verlag, Germany, March 2004.
• [29] Farahbod, R., Glässer, U., Vajihollahi,M.: Abstract Operational Semantics of the Business Process Execution Language for Web Services, Technical Report SFU-CMPT-TR-2005-04, Simon Fraser University, Feb. 2005, Revised version of SFU-CMPT-TR-2004-03, April 2004.
• [30] Farahbod, R., Glässer, U., Vajihollahi,M.: A Formal Semantics for the Business Process Execution Language for Web Services, Web Services and Model-Driven Enterprise Information Systems (S. Bevinakoppa, et al., Eds.), INSTICC Press, Portugal, May 2005.
• [31] Farahbod, R., et al.: The CoreASM Project, http://www.coreasm.org.
• [32] Gargantini, A., Riccobene, E., Rinzivillo, S.: Using Spin to Generate Tests from ASM Specifications, Abstract State Machines 2003, Springer, 2003.
• [33] Glässer, U., Gotzhein, R., Prinz, A.: The formal semantics of SDL-2000: status and perspectives, Comput. Networks, 42(3), 2003, 343-358.
• [34] Glässer, U., Gu, Q.-P.: Formal Description and Analysis of a Distributed Location Service for Mobile Ad Hoc Networks, Theoretical Computer Science, 336, May 2005, 285-309.
• [35] Glässer, U., Gurevich, Y., Veanes, M.: Abstract CommunicationModel for Distributed Systems, IEEE Trans. on Soft. Eng., 30(7), July 2004, 458-472.
• [36] Gurevich, Y.: Evolving Algebras 1993: Lipari Guide, in: Specification and Validation Methods (E. Börger, Ed.), Oxford University Press, 1995, 9-36.
• [37] Gurevich, Y.: Sequential Abstract State Machines Capture Sequential Algorithms, ACM Transactions on Computational Logic, 1(1), July 2000, 77-111.
• [38] Gurevich, Y., Huggins, J.: Evolving Algebras and Partial Evaluation, IFIP 13th World Computer Congress (B. Pehrson, I. Simon, Eds.), I: Technology/Foundations, Elsevier, Amsterdam, the Netherlands, 1994.
• [39] Gurevich, Y., Tillmann, N.: Partial Updates: Exploration, Journal of Universal Computer Science, 7(11), 2001, 917-951.
• [40] Gurevich, Y., Tillmann, N.: Partial Updates, Journal of Theoretical Computer Science, 336(2-3), 2005, 311-342.
• [41] Huckle, T.: Collection of Software Bugs, Technical report, Technical University Munich, 2004, Last visited Sep. 2005, http://www5.in.tum.de/_huckle/bugse.html.
• [42] Huggins, J.: An Offline Partial Evaluator for Evolving Algebras, Technical Report CSE-TR-229-95, University of Michigan, 1995.
• [43] ITU-T Recommendation Z.100 Annex F (11/00): SDL Formal Semantics Definition, International Telecommunication Union, 2001.
• [44] Kappel, A. M.: Executable Specifications Based on Dynamic Algebras, in: Logic Programming and Automated Reasoning (A. Voronkov, Ed.), vol. 698 of Lecture Notes in Artificial Intelligence, Springer, 1993, 229-240.
• [45] Memon, M. A.: Specification Language Design Concepts: Aggregation and Extensibility in CoreASM, Master Thesis, Simon Fraser University, Burnaby, Canada, April 2006.
• [46] Microsoft FSE Group: The Abstract State Machine Language, Last visited June 2003, http://research. microsoft.com/fse/asml/.
• [47] Müller, W., Ruf, J., Rosenstiel, W.: An ASM Based SystemC Simulation Semantics., SystemC - Methodologies and Applications (W. Müller, J. Ruf, W. Rosenstiel, Eds.), Kluwer Academic Publishers, June 2003.
• [48] R. Eschbach and U. Glässer and R. Gotzhein and M. von Löwis and A. Prinz: Formal Definition of SDL-2000: Compiling and Running SDL Specifications as ASMModels, Journal of Universal Computer Science, 7(11), 2001, 1024-1049.
• [49] Schmid, J.: Executing ASM Specitications with AsmGofer, Last visited Sep. 2005, www.tydo.de/ AsmGofer/.
• [50] Schmid, J.: Compiling Abstract State Machines to C++, Journal of Universal Computer Science, 7(11), 2001, 1068-1087.
• [51] Stärk, R., Schmid, J., Börger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation, Springer-Verlag, 2001.