Abstract
This paper presents Genesys, a framework for the high-level construction of property conform code generators. Genesys is an integral part of jABC, a flexible framework designed to enable a systematic model-driven development of systems and applications on the basis of an (extensible) library of well-defined, reusable building blocks. Within jABC, Genesys manages the construction of code generators for jABC’s models. So far, Genesys has been used to develop code generators for a variety of different target platforms, like a number of Java-based platforms, mobile devices, BPEL engines, etc. Since the code generators are themselves built within the jABC in a model-driven way, concepts like bootstrapping and reuse of existing components enable a fast evolution of Genesys’ code generation library, and a high degree of self-application. Due to its increasing complexity and its high degree of reuse, Genesys profits from model checking-based verification. This way, jABC’s models of code generators can be automatically checked wrt. well-formedness properties, to ensure that the models do indeed only consist of building blocks which are suitable for the considered target platforms, and whose versions are mutually compatible. It can be also be verified that the code generation process only starts after a successful initialization phase, and that the generated code is always packaged with all the required libraries. We will illustrate the ease of extension and flexibility of the Genesys framework by describing the intended coverage of diversity while highlighting the high potential of reuse.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Hoare CAR (2003) The verifying compiler: a grand challenge for computing research. J ACM 50(1):63–69
Hoare CAR, Misra J (2005) Verified software: theories, tools, experiments. Vision of a Grand Challenge Project. In: Proc. VSTTE. Springer Verlag, Zürich, Switzerland
Appel AW (2001) Foundational Proof-Carrying Code. In: Proc. LICS ’01, p 247. IEEE Computer Society
Necula GC (1997) Proof-carrying code. In: Proc. POPL ’97, ACM Press, New York, NY, USA, pp 106–119
Denney E, Fischer B (2006) Extending source code generators for evidence-based software certification. In: Proc. ISOLA ’06, pp 138–145
Goos G, Zimmermann W (1999) Verification of Compilers. In: Correct System Design, vol 1710. Springer, Berlin, pp 201–230. http://www.info.uni-karlsruhe.de/papers/CorrectSystemDesign99.ps.gz
Necula GC (2000) Translation validation for an optimizing compiler. ACM SIGPLAN Notices 35(5): 83–94
Stürmer I, Weinberg D, Conrad M (2005) Overview of existing safeguarding techniques for automatically generated code. In: Proc. SEAS ’05, ACM Press, New York, NY, USA, pp 1–6
Coglio A, Green C (2005) A constructive approach to correctness, exemplified by a generator for certified Java Card Applets. In: Proc. VSTTE
Margaria T, Steffen B (2004) Lightweight coarse-grained coordination: a scalable system-level approach. STTT 5(2–3): 107–123
Margaria T, Steffen B, Reitenspieß M (2005) Service-oriented design: the roots. In: ICSOC 2005: 3rd ACMSIGSOFT/SIGWEB Int. Conf. on Service-Oriented Computing, LNCS N.3826, Springer, Amsterdam, pp 450–464
Margaria T, Steffen B (2006) Service engineering: linking business and IT. IEEE Comput 39(10): 45–55
Steffen B, Margaria T, Nagel R, Jörges S, Kubczak C (2006) Model-Driven Development with the jABC. In: HVC—IBM Haifa Verification Conference, LNCS N.4383. Springer, Berlin, pp 92–108
Technische Universität Dortmund: jABC Website (2007). http://www.jabc.de
OASIS: WS-BPEL 2.0 Specification (2007). http://docs.oasis-open.org/wsbpel/2.0/wsbpel-v2.0.pdf
Hansen J (2007) NBC/NXC—Next Byte Codes & Not eXactly C. http://bricxcc.sourceforge.net/nbc/
Clarke EM, Grumberg O, Peled D (2001) Model checking. MIT Press, Cambridge, MA, USA
Queille JP, Sifakis J (1982) Specification and verification of concurrent systems in CESAR. In: Proc. 5th Colloquium on International Symposium on Programming. Springer, London, UK, pp 337–351
Margaria T, Steffen B (2008) Agile IT: thinking in user-centric models. In: Proc. ISoLA 2008, CCIS N.17, Springer, pp 493–505
Margaria T, Steffen B (2008) Business process modelling in the jABC: the one-thing approach. In: Handbook of research on business process modeling. IGI Global
Steffen B, Narayan P (2007) Full life-cycle support for end-to-end processes. IEEE Computer 40(11): 64–73
ITU: General recommendations on telephone switching and signaling-intelligent network: Introduction to intelligent network capability set 1, Recommendation Q.1211. Tech. rep., Standardization Sector of ITU, Geneva (1993)
ITU-T: Recommendation Q.1203. Intelligent Network–Global Functional Plane Architecture. Tech. rep., Standardization Sector of ITU (1992)
Apache Software Foundation: Velocity Website (2007). http://velocity.apache.org/
The jABC Team (2008) jABC Common Sibs. http://www.jabc.de/sib
Niemeyer P (2008) BeanShell—lightweight scripting for Java. http://www.beanshell.org/
The Codehaus (2008) Groovy Website. http://groovy.codehaus.org/
Müller-Olm M, Schmidt D, Steffen B (1999) Model-checking: a tutorial introduction. In: Proc. SAS, pp 330–354
Steffen B, Margaria T, Braun V, Kalt N (1997) Hierarchical service definition. In: Annual Review of Communication. Int. Engineering Consortium Chicago (USA), IEC, pp 847–856
Bakera M, Margaria T, Renner CD, Steffen B (2008) Model checking with the JavaABC Framework—from METAGame to GEAR. In: QEES’08, Intern. Symposium on Quality Engineering for Embedded Systems—In conjunction with the ECMDA 2008. IEEE CS
Bakera M, Margaria T, Renner CD, Steffen B (2008) Verification, diagnosis and adaptation: tool-supported enhancement of the model-driven verification process. Innov Syst Softw Eng NASA J (in press)
Bakera M, Margaria T, Renner CD, Steffen B (2007) Verification, diagnosis and adaptation: tool supported enhancement of the model-driven verification process. In: ISoLA 2008 Workshop, pp 85–97
Lecarme O, Peyrolle-Thomas M-C (1978) Self-compiling Compilers: An Appraisal of their Implementation and Portability. Softw. Pract. Exp. 8(2): 149–170
AndroMDA Website (2008). http://www.andromda.org/
Engeler E (1971) Structure and meaning of elementary programs. In: Symposium on Semantics of Algorithmic Languages. Springer, Berlin. Lect. Notes in Mathematics, vol 188
Andrews P, Stuber J, Griffiths L, Bagnall B, Scholz M, Rinkens T, Solorzano J (2008) lejos website. http://lejos.sourceforge.net/
Jörges S, Kubczak C, Pageau F, Margaria T (2007) Model driven design of reliable robot control programs using the jABC. In: Proc. EASe’07, pp 137–148
Schulte BE (2007) Modellgetriebene Steuerung eingebetteter Systeme und ihre Anwendung für Lego NXT. Master’s thesis, Chair for Programming Systems, Technische Universität Dortmund
SUN Microsystems (2008) The Java ME Platform. http://java.sun.com/javame/index.jsp
SUN Microsystems (2008) Connected Limited Device Configuration (CLDC). http://java.sun.com/products/cldc/
Active Endpoints: The ActiveBPEL Community Edition Engine (2008) http://www.activevos.com/community-open-source.php
Gaeb J (2007) Entwicklung eines BPEL-Plugins für das jABC-Framework. Master’s thesis, Chair for Programming Systems, Technische Universität Dortmund
W3C (2008) W3C Document Object Model. http://www.w3.org/DOM/
Hösel S (2008) Entwicklung eines Plug-ins für das jABC-Framework zur Integration von .NET mittels C#. Master’s thesis, Service and Software Engineering, Universität Potsdam
Jörges S, Margaria T, Steffen B (2006) FormulaBuilder: a tool for graph-based modelling and generation of formulae. In: Proc. ICSE’06, pp 815–818
Dwyer M, Avrunin G, Corbett J (1999) Patterns in property specifications for finite-state verification. In: Proc. ICSE ’99, pp 411–420. IEEE CS Press
Kozen D (1983) Results on the propositional mu-calculus. Theor Comput Sci 27: 333–354
SUN Microsystems (2008) Java EE at a Glance. http://java.sun.com/javaee/
SUN Microsystems (2008) Enterprise JavaBeans Technology. http://java.sun.com/products/ejb/
SWS Challenge Website (2008). http://sws-challenge.org
Arenas A, Bicarregui J, Margaria T (2006) The FMICS view on the verified software repository. J Integ Des Process Sci 10: 47–54
Margaria T, Kubzcak C, Steffen B (2008) Bio-jeti: a service integration, design, and provisioning platform for orchestrated bioinformatics processes. BioMed Central (BMC) Bioinformatics 2008; Supplement dedicated to Network Tools and Applications in Biology 2007 Workshop (NETTAB 2007) ISSN 1471-2105. Published online 2008 April 25. 9(Suppl 4):S12. doi:10.1186/1471-2105-9-S4-S12
Steffen B, Margaria T, Nagel R (2005) Remote integration and coordination of verification tools in jETI. In: Proc. ECBS 2005, 12th IEEE Int. Conf. on the Engineering of Computer Based Systems, pp 431–436. IEEE Computer Soc. Press, Greenbelt (USA)
W3C (2008) Web Services Description Working Group (Specifications & Drafts). http://www.w3.org/2002/ws/desc/
W3C (2008) W3C XML Protocol Working Group. http://www.w3.org/2000/xp/Group/
jax-ws: JAX-WS Reference Implementation (2008). http://jax-ws.dev.java.net/
Kubczak C, Margaria T, Steffen B, Nagel R (2008) Service-oriented mediation with jABC/jETI. In: Petrie C, Margaria T, Zaremba M, Lausen H (eds) Semantic Web services challenge—results from the first year. Springer, Berlin, pp 71–99 (in press)
Margaria T, Bakera M, Kubczak C, Naujokat S, Steffen B (2008) Automatic generation of the SWS-challenge mediator with jABC/ABC. In: Petrie C, Margaria T, Zaremba M, Lausen H (eds) Semantic Web Services challenge - results from the first year. Springer, Berlin, pp 119–138 (in press)
W3C (2008) W3C XML Schema. http://www.w3.org/XML/Schema
Lamprecht AL, Margaria T, Steffen B (2006) Data-flow analysis as model checking within the jABC. In: CC, pp 101–104
Steffen B (1991) Data flow analysis as model checking. In: TACS ’91: Proceedings of the International Conference on Theoretical Aspects of Computer Software. Springer, Berlin, pp 346–365
Niese O, Steffen B, Margaria T, Hagerer A, Brune G, Ide HD (2001) Library-based design and consistency checking of system-level industrial test cases. In: Proc. FASE 2001, LNCS, vol 2029. Springer, Berlin, pp 233–248
Object Mentor: JUnit Website (2007). http://www.junit.org/
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Jörges, S., Margaria, T. & Steffen, B. Genesys: service-oriented construction of property conform code generators. Innovations Syst Softw Eng 4, 361–384 (2008). https://doi.org/10.1007/s11334-008-0071-2
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11334-008-0071-2