The Object Constraint Language (OCL) has become an essential part of many model-driven engineering (MDE) approaches and tools, adding precision and semantic detail to software models such as class diagrams, and defining transformation rules in model transformation languages. The many uses of OCL have led to its extension beyond the official standard (version 2.4), to add new types and language elements, such as procedural statements. In this paper we identify how the operational semantics of the OCL standard can be extended to include map, reference and function types and procedural statements, and we describe applications of the semantics to emulation, analysis and validation of OCL specifications.

Many organizations rely on software systems to accomplish their daily operations. Over time, these systems require maintenance and need to evolve to meet new requirements and stakeholder needs. Visual representations and textual abstractions are important to support the understanding of these systems for their maintenance and evolution. Reverse engineering is used to generate such representations and software models by abstracting various types of diagrams from code bases, and Model-Driven Engineering (MDE) provides a rigorous means of facilitating the reverse engineering process, enabling the generation of formal visual and textual models with a precise semantic alignment to the source code. Large language models (LLMs) are increasingly used in various fields, including software engineering. Yet, they have rarely been used to abstract software models from source code. In this paper, we present a new Model-Driven Reverse Engineering (MDRE) approach for abstracting Unified Modeling Language (UML) and Object Constraint Language (OCL) representations from software systems for understanding and documenting them. To improve the usability and scope of MDRE, we use LLMs to abstract UML class diagrams and OCL specifications from Java and Python programs. Case studies are conducted to evaluate the proposed approach and to encourage maintainers to leverage LLMs in the reverse engineering process, thereby improving their understanding and maintenance of Java- and Python-based systems.

Using reverse engineering to extract semantic representations from software systems is beneficial for the understanding of these systems, and can facilitate their maintenance and evolution. In particular, extracting semantically-precise specifications from systems is useful for re-engineering of systems to functionally-equivalent versions in different programming languages. Large language models (LLMs) are a type of machine learning (ML) technique that has been utilized in various domains, including software engineering and program translation. Yet, abstracting precise Object Constraint Language (OCL) specifications from source code using LLMs has not gained attention in reverse engineering approaches. In this paper, we present a new reverse engineering approach, named LLM4Models, to abstract OCL specifications from Java and Python programs, using LLMs.

Abstract The porting or translation of software applications from one programming language to another is a common requirement of organisations that utilise software, and the increasing number and diversity of programming languages makes this capability as relevant today as in previous decades. Several approaches have been used to address this challenge, including machine learning and the manual definition of direct language-to-language translation rules, however the accuracy of these approaches remains unsatisfactory. In this paper we describe a new approach to program translation using model-driven engineering techniques: reverse-engineering source programs into specifications in the UML and OCL formalisms, and then forward-engineering the specifications to the required target language. This approach can provide assurance of semantic preservation, and additionally has the advantage of extracting precise specifications of software from code. We provide an evaluation based on a comprehensive dataset of examples, including industrial cases, and compare our results to those of other approaches and tools. Our specific contributions are: (1) Reverse-engineering source programs to detailedsemantic modelsof software behaviour, to enable semantically-correct translations and reduce re-testing costs; (2) Program abstraction processes defined by precise and explicit rules, which can be edited and configured by users; (3) A set of reusable OCL library components appropriate for representing program semantics, and which can also be used for OCL specification of new applications; (4) A systematic procedure for building program abstractors based on language grammars and semantics.

Abstract Requirements Engineering (RE) has undergone several transitions over the years, from traditional methods to agile approaches emphasising increased automation. In many software development projects, requirements are expressed in natural language and embedded within large volumes of text documents. At the same time, RE activities aim to define software systems' functionalities and constraints. However, manually executing these tasks is time-consuming and prone to errors. Numerous research efforts have proposed tools and technologies for automating RE activities to address this challenge, which are documented in published works. This review aims to examine empirical evidence on automated RE and analyse its impact on the RE sub-domain and software development. To achieve our goal, we conducted a Systematic Literature Review (SLR) following established guidelines for conducting SLRs. We aimed to identify, aggregate, and analyse papers on automated RE published between 1996 and 2022. We outlined the output of the support tool, the RE phase covered, levels of automation, development approach, and evaluation approaches. We identified 85 papers that discussed automated RE from various perspectives and methodologies. The results of this review demonstrate the significance of automated RE for the software development community, which has the potential to shorten development cycles and reduce associated costs. The support tools primarily assist in generating UML models (44.7%) and other activities such as omission of steps, consistency checking, and requirement validation. The analysis phase of RE is the most widely automated phase, with 49.53% of automated tools developed for this purpose. Natural language processing technologies, particularly POS tagging and Parser, are widely employed in developing these support tools. Controlled experimental methods are the most frequently used (48.2%) for evaluating automated RE tools, while user studies are the least employed evaluation method (8.2%). This paper contributes to the existing body of knowledge by providing an updated overview of the research literature, enabling a better understanding of trends and state-of-the-art practices in automated RE for researchers and practitioners. It also paves the way for future research directions in automated requirements engineering.

Abstract Testing is one of the most time‐consuming and unpredictable processes within the software development life cycle. As a result, many test case optimization (TCO) techniques have been proposed to make this process more scalable. Object Constraint Language (OCL) was initially introduced as a constraint language to provide additional details to Unified Modeling Language models. However, as OCL continues to evolve, an increasing number of systems are being expressed by this language. Despite this growth, a noticeable research gap exists for the testing of systems whose specifications are expressed in OCL. In our previous work, we verified the effectiveness and efficiency of performing the test case prioritization (TCP) process for these systems. In this study, we extend our previous work by integrating the test case minimization (TCM) process to determine whether TCM can also benefit the testing process under the context of OCL. The evaluation of TCO approaches often relies on well‐established metrics such as the average percentage of fault detection (APFD). However, the suitability of APFD for model‐based testing (MBT) is not ideal. This paper addresses this limitation by proposing a modification to the APFD metric to enhance its viability for MBT scenarios. We conducted four case studies to evaluate the feasibility of integrating the TCM and TCP processes into our proposed approach. In these studies, we applied the multi‐objective optimization algorithm NSGA‐II and the genetic algorithm independently to the TCM and TCP processes. The objective was to assess the effectiveness and efficiency of combining TCM and TCP in enhancing the testing phase. Through experimental analysis, the results highlight the benefits of integrating TCM and TCP in the context of OCL‐based testing, providing valuable insights for practitioners and researchers aiming to optimize their testing efforts. Specifically, the main contributions of this work include the following: (1) we introduce the integration of the TCM process into the TCO process for systems expressed by OCL. This integration benefits the testing process further by reducing redundant test cases while ensuring sufficient coverage. (2) We comprehensively analyze the limitations associated with the commonly used metric, APFD, and then, a modified version of the APFD metric has been proposed to overcome these weaknesses. (3). We systematically evaluate the effectiveness and efficiency of OCL‐based TCO processes on four real‐world case studies with different complexities.

Software complexity has become a significant social problem, which MDE endeavours to alleviate, however MDE approaches and tools often introduce additional complexity which prevents general software practitioners from benefiting from MDE solutions. In this paper we present an alternative approach for MDE in the domain of language processing, using lightweight tools (Antlr and CGTL) suitable for general industrial use. We evaluate the approach on tasks of DSL definition, software abstraction, and program translation, based on our experience with industrial applications of MDE.

Abstract Model‐Driven Development (MDD) is one of the important approaches to develop complex software systems. This approach tries to model a system in high‐abstraction level. Then through applying multiple transformations step by step, the model abstraction level is reduced and finally yields to executable code. As a result, Model transformation (MT) plays a pivotal role on the realization of MDD goals. Due to the increasing complexity of software systems, MTs naturally become more complex. Hence, qualitative technical issues may be overlooked or forgotten in these model transformations. To alleviate these issues in terms of technical debts/code smells in MTs, we can apply MT patterns. A main drawback on applying patterns is that most of them are cataloged in informal language. Additionally, construction of a conceptual framework to help MT designers through applying patterns requires a precise specification of the underlying MT patterns. With a formal basis, this paper is trying to realize the proposed framework. Hence, some of the existing well‐known MT patterns are formalized. Then based on the identified common technical debts/code smells in MTs, a designer can be directed to apply the appropriate patterns and resolve the detected problems iteratively. For the applicability and functionality of the proposed framework, several examples of problematic model transformations in terms of quality flaws were considered and resolved using the appropriate patterns. We consider the Epsilon Transformation Language (ETL) cases of model transformations in this paper, and other similar MT languages could be treated using the same measures and patterns as well.

Abstract Model transformation has become an established field, and it is important to improve the quality of specifications written in transformation languages. Different transformation patterns have been introduced in the model‐driven engineering (MDE) community to improve the quality of transformation specifications. However, due to the different definitions of pattern concepts by different authors, it is difficult for practitioners to understand how to apply patterns in practice. Therefore, there is a need to unify transformation pattern concepts by presenting a generic metamodel and formalizing patterns in terms of this metamodel, to define the meaning of pattern application. In this research a general metamodel for definition of different design patterns in model transformation is provided. The metamodel presents clear description of common aspects of transformation patterns, which facilitates the application of patterns on model transformations by validating the application against the underlying formalism. Additionally, a unified and precise terminology for the application and verification of model transformation patterns by using a formal model of model transformation patterns in the Z notation is presented. To show the applicability of the proposed formalism, four well‐known model transformation patterns are specified.

In this article, we address how the production of model transformations (MT) can be accelerated by automation of transformation synthesis from requirements, examples, and metamodels. We introduce a synthesis process based on metamodel matching, correspondence patterns between metamodels, and completeness and consistency analysis of matches. We describe how the limitations of metamodel matching can be addressed by combining matching with automated requirements analysis and model transformation by example (MTBE) techniques. We show that in practical examples a large percentage of required transformation functionality can usually be constructed automatically, thus potentially reducing development effort. We also evaluate the efficiency of synthesised transformations. Our novel contributions are: The concept of correspondence patterns between metamodels of a transformation. Requirements analysis of transformations using natural language processing (NLP) and machine learning (ML). Symbolic MTBE using “predictive specification” to infer transformations from examples. Transformation generation in multiple MT languages and in Java, from an abstract intermediate language.

Abstract The QVT-Relations (QVT-R) model transformation language is an OMG standard notation for model transformation specification. It is highly declarative and supports (in principle) bidirectional (bx) transformation specification. However, there are many unclear or unsatisfactory aspects to its semantics, which is not precisely defined in the standard. UML-RSDS is an executable subset of UML and OCL. It has a precise mathematical semantics and criteria for ensuring correctness of applications (including model transformations) by construction. There is extensive tool support for verification and for production of 3GL code in multiple languages (Java, C#, C++, C, Swift and Python). In this paper, we define a translation from QVT-R into UML-RSDS, which provides a logically oriented semantics for QVT-R, aligned with the RelToCore mapping semantics in the QVT standard. The translation includes variation points to enable specialised semantics to be selected in particular transformation cases. The translation provides a basis for verification and static analysis of QVT-R specifications and also enables the production of efficient code implementations of QVT-R specifications. We evaluate the approach by applying it to solve benchmark examples of bx.

In this paper, we present a Systematic Literature Review (SLR) on combining Agile development and Model-Driven Development (MDD). The objectives of this paper are to identify what are the main characteristics of current Agile Model-Driven Development (Agile MDD) approaches, as well as the benefits and the problems of adopting these approaches. Fifteen publications have been identified and selected as primary studies on which we conducted the analysis. The results show that Agile development and MDD can coexist and benefit from their integration. However, combining Agile and MDD is still in its early stages and more eort is required in research to advance this area. The main contributions of this paper are: detailed and condensed results in the context of current Agile MDD approaches, detailed results on the benefits of Agile MDD in practice, and the observed problems and challenges of the current Agile MDD approaches.

Abstract A model transformation verification task may involve a number of different transformations, from one or more of a wide range of different model transformation languages, each transformation may have a particular transformation style, and there are a number of different verification properties which can be verified for each language and style of transformation. Transformations may operate upon many different modelling languages. This diversity of languages and properties indicates the need for a suitably generic framework for model transformation verification, independent of particular model transformation languages, and able to provide support for systematic procedures for verification across a range of languages, and for a range of properties. In this paper we describe the elements of such a framework, and apply this framework to some example transformation verification problems. The paper is novel in covering a wide range of different verification techniques for a wide range of MT languages, within an integrated framework.

Elasticity refers to the auto-scaling ability of clouds towards optimally matching their resources to actual demand conditions. An important problem facing the infrastructure and service providers is how to optimise their resource configurations online, to elastically serve time-varying demands. Most scaling methodologies provide resource reconfiguration decisions to maintain quality properties under environment changes. However, issues related to the timeliness of such reconfiguration decisions are often neglected. In this paper, we present a methodology for online optimisation of cloud configurations. We first employ a search-based approach to extract near-optimal configurations considering conflicting performance and business quality attributes. Towards reducing the burden of time-consuming evaluations of configurations' quality, we develop surrogate models to predict their quality based on history observations. Finally, we evaluate our technique using Cloud Sim-based cloud simulation. Our experimental results show that the use of surrogates can produce high quality configurations with lead time of seconds and prediction error within 6%.

This paper defines a catalogue of patterns for the specification and design of model transformations, and provides a systematic scheme and classification of these patterns, together with pattern application examples in leading model transformation languages such as ATL, QVT, GrGen.NET, and others. We consider patterns for improving transformation modularization and efficiency and for reducing data storage requirements. We define a metamodel-based formalization of model transformation design patterns, and measurement-based techniques to guide the selection of patterns. We also provide an evaluation of the effectiveness of transformation patterns on a range of different case studies.

The requirement for elasticity involves the ability of cloud data centers to add or remove resources at a fine grain and with a lead time of seconds, closely matching resources to the actual demand conditions. Elasticity techniques can assist cloud stakeholders in regards to: (i) alleviating data center capital and operating costs, (ii) keeping cloud services continuously available, (iii) supporting market flexibility. To date, most infrastructure scaling methodologies can provide resource reconfiguration decisions to maintain quality properties under environment changes. However, issues related to the timeliness of reconfiguration decisions under dynamic changes are not adequately addressed. In this paper, we describe the PhD motivation, research questions and methodology towards developing cloud infrastructure and hosted services QoS optimisations under environment uncertainties.

As Cloud Computing becomes more predominant, large scale datacenters are subject to an increasing demand for efficiency and flexibility. However, growing infrastructure management complexity and maintenance costs are becoming a hindrance to the advancement of the Cloud vision. In this paper we discuss how existing datacenter resource management approaches fail to provide infrastructure elasticity and suggest a resources provisioning architecture to fill this gap. As a first step towards implementing our targets, we present a metamodel to describe the characteristics of the Cloud landscape, emphasising on a provider’s perspective. With this meta-model we intend to introduce new modelling concepts towards facilitating the selection of optimal reconfigurations in a timely fashion. 1

This paper introduces Model Projection. Finite state models such as Extended Finite State Machines are being used in an ever increasing number of software engineering activities. Model projection facilitates model development by specializing models for a specific operating environment. A projection is useful in many design-level applications including specification reuse and property verification.

Identifying and resolving design problems in the early design phase can help ensure software quality and save costs. There are currently few tools for analyzing designs expressed using the Unified Modeling Language (UML). Tools such as OCLE and USE support analysis of static structural properties. These tools provide mechanisms for checking instance models against invariant properties expressed using the object constraint language (OCL). In this paper we propose an approach to analyzing behavioral properties of UML models that can utilize static analysis tools. The approach includes a technique for generating a class model of behavior from operation specifications expressed in a restricted form of OCL Behavioral properties are expressed as invariants defined in the class model of behavior. Static analysis tools such as USE and OCLE can be used to check object models describing series of snapshots. Most of the analysis can be automated. We illustrate our approach by analyzing static separation of duty and dynamic separation of duty properties of a hierarchical role-based access control model (HRBAC).

Interaction diagrams are a widely-used UML notation, however in contrast to class diagrams or state machines there is a lack of formal semantics for interaction diagrams. We propose a formal semantics for the notation, and consider applications of this semantics for checking the consistency of interaction diagrams with other UML models, and for diagrammatic formal specification of real-time properties.

B has been widely used for high-integrity systems development, for example in the railway industry. However, there are few published guidelines on how to structure B specifications for particular types of system, such as reactive control systems. In this paper, we describe a method to support the graphical design of systems using the B abstract machine notation (AMN), and we develop guidelines for expressing the structuring requirements of reactive systems in B.

The Fusion and Syntropy object-oriented methods reflect some of the most rigorous object-oriented modelling concepts and experiences currently available. In this paper we identify similarities and differences between the two methods, and discuss how the best concepts from each of these methods can be combined to obtain clearer, more precise analysis models, specifications, and designs, and can be used to enhance the modelling power of the other. A summary of a semantics for Syntropy is given in Appendix A, and ways in which this can be extended to Fusion are described. This work was carried out as part of the EPSRC projects ‘Object-oriented Specification of Reactive and Real-time Systems’ concerning the extension of Fusion to treat reactive systems, and ‘Formal Underpinnings for Object Technology’ concerned with developing a full semantics for Syntropy.

The paper describes experience of a large-scale application of the Z specification language to the formalisation of parts of the transformation and analysis functionality contained in a static analysis toolset for COBOL. Aspects of the development described in the paper are: the combination of 'diagrammatic' analysis and design techniques with formal specification, in order to obtain well-structured and comprehensible specifications; techniques to utilise object-oriented structure in the domain in order to structure a specification; benefits of using formal specifications in an industrial environment in which expertise in formal methods was restricted, and which was predominately within a traditional database and imperative programming culture.

The paper describes approaches to the specification and design of a controller for a gas burner system using VDM/sup ++/. It defines a systematic method for interpreting declarative requirements statements in real-time temporal logic, and for the construction of abstract and concrete VDM/sup ++/ specifications which implement the formalised requirements. Timing analysis is also addressed. The central contribution of the paper is a primarily mechanical process of refinement from abstract declarative specifications of a control problem to implemented controllers in Ada95.

Abstract This paper describes an approach to the semantic analysis of procedural code. The techniques differ from those adopted in current static analysis tools such as MALPAS (Bramson, 1984) and SPADE (Clutterbuck and Carré, 1988) in two key respects: (1) A database is used, together with language‐specific and language‐independent data models, as a repository for all information about a program or set of programs which is required for analysis, and for storing and interrelating the results of analyses; (2) The techniques aim to treat the full language under consideration by a process of successive transformation and abstraction from the source code until a representation is obtained which is amenable to analysis. This abstraction process can include the production of formal specifications from code. The techniques have been partially implemented for the OS/VS IBM diallect of COBOL '74 and for FORTRAN '77. Several components of the resulting toolset have been formally specified in Z, thus meeting some of the integrity requirements for verification tools given in ‘The procurement of safety critical software in defence equipment’ (MoD, 1991). The techniques have been applied in practice to a wide range of source programs and analysis problems (Lano and Haughton, 1993b; Lano, et al., 1991), including assessment problems (Lloyd's Register, 1992, 1993; Hornsby and Eldridge, 1990). Section 1 gives an overview of the analysis process. Section 2 describes the representations used to support the process. Section 3 describes some of the techniques involved, and Section 4 gives examples of applications of the process. The Appendix contains extracts from a large case study carried out using tools developed to support the process.

Abstract We describe methods and software tools which aid in reverse‐engineering COBOL application programs back to specifications (and in validating them against specifications). The aim is to create object‐based abstractions from the implementation to capture design and functionality. The central process which the tools support is ‘transformation from formalism to formalism’, first from COBOL to the intermediate language Uniform, then from Uniform to a functional description language, and then to the specification language Z. In the process, dataflow diagrams, entity‐relationship diagrams and call‐graphs, and other types of information, are extracted from the code.

The authors provide insights into the process of deriving objects from code and specifications. Their purpose is to facilitate the more general process of reverse engineering. They concentrate on a method for object identification and give some examples of deriving objects with details on the syntax of the object-oriented notation Z++. The authors provide some further examples of object derivation, concentrating on internal data structures in program code. They detail the relationship between objects and abstract data types, and discuss the concepts of reusability with respect to inheritance hierarchies.>

The mathematical treatment of the concepts of vagueness and approximation is of increasing importance in artificial intelligence and related research. The theory of fuzzy sets was created by Zadeh [Z] to allow representation and mathematical manipulation of situations of partial truth, and proceeding from this a large amount of theoretical and applied development of this concept has occurred. The aim of this paper is to develop a natural logic and set theory that is a candidate for the formalisation of the theory of fuzzy sets. In these theories the underlying logic of properties and sets is intuitionistic, but there is a subset of formulae that are ‘crisp’, classical and two-valued, which represent the certain information. Quantum logic or logics weaker than intuitionistic can also be adopted as the basis, as described in [L]. The relationship of this theory to the intensional set theory MZF of [Gd] and the global intuitionistic set theory GIZF of Takeuti and Titani [TT] is also treated.

Abstract Reverse‐engineering application codes back to the design and specification stage may entail the recreation of lost information for an application, or the extraction of new information. We describe techniques which produce abstractions in object‐oriented and functional notations, thus aiding the comprehension of the essential structure and operations of the application, and providing formal design information which may make the code much more maintainable and certainly more respectable. The two types of application considered here are (1) data processing applications written in COBOL — of primary importance owing to their predominance in present computing practice — and (2) scientific applications written in FORTRAN. These two require somewhat different abstraction approaches.

Abstract In this paper we define a language, Z++, and a method based upon this language, to support the use of formal methods in software maintenance. Formal methods have been proposed several times as the solution to the growing problem of software maintenance, and we base our approach on the more successful of the attempts made to apply these methods. Our approach is to use a conceptually simple framework, based on an object‐oriented extension to the specification language Z (Spivey, 1989), for dealing with requests for changes to software for which some formal documentation and record of development already exists. The method is centered on the maintenance of the specifications and the development record, not upon source code or Structured Methodology documentation. It is proposed as a practical approach for software in the medium‐term future, allowing the mass of programming detail that makes the code maintenance problem so expensive to be ignored. Therefore changes and extensions to application systems can be made more rapidly. We describe the language and give details of the specification and refinement system, together with a description of the current state of the implementation of this system.