Alliance of model-driven engineering with a proof-based formal approach

Model-driven engineering (MDE) promotes the use of models throughout the software development cycle in order to increase abstraction and reduce software complexity. It favors the definition of domain-specific modeling languages (DSMLs) thanks to frameworks dedicated to meta-modeling and code generation like EMF (Eclipse Modeling Framework). The standard semantics of meta-models allows interoperability between tools such as language analysers (e.g., XText), code generators (e.g., Acceleo), and also model transformation tools (e.g., ATL). However, a major limitation of MDE is the lack of formal reasoning tools allowing to ensure the correctness of models. Indeed, most of the verification activities offered by MDE tools are based on the verification of OCL constraints on instances of meta-models. However, these constraints mainly deal with structural properties of the model and often miss out its behavioral semantics. In this work, we propose to bridge the gap between MDE and the rigorous world of formal methods in order to guarantee the correctness of both structural and behavioral properties of the model. Our approach translates EMF meta-models into an equivalent formal B specification and then injects models into this specification. The equivalence between the resulting B specification and the original EMF model is kept by proven design steps leading to a rigorous MDE technique. The AtelierB prover is used to guarantee the correctness of the model’s behavior with respect to its invariant properties, and the ProB model-checker is used to animate underlying execution scenarios which are translated back to the initial EMF model. Besides the use of these automatic reasoning tools in MDE, proved B refinements are also investigated in this paper in order to gradually translate abstract EMF models to concrete models which can then be automatically compiled into a programming language.

     

Model-driven engineering: A survey supported by the unified conceptual model

During the last decade a new trend of approaches has emerged, which considers models not just documentation artefacts, but also central artefacts in the software engineering field, allowing the creation or automatic execution of software systems starting from those models. These proposals have been classified generically as Model-Driven Engineering (MDE) and share common concepts and terms that need to be abstracted, discussed and understood. This paper presents a survey on MDE based on a unified conceptual model that clearly identifies and relates these essential concepts, namely the concepts of system, model, metamodel, modeling language, transformations, software platform, and software product. In addition, this paper discusses the terminologies relating MDE, MDD, MDA and others. This survey is based on earlier work, however, contrary to those, it intends to give a simple, broader and integrated view of the essential concepts and respective terminology commonly involved in the MDE, answering to key questions such as: What is a model? What is the relation between a model and a metamodel? What are the key facets of a modeling language? How can I use models in the context of a software development process? What are the relations between models and source code artefacts and software platforms? and What are the relations between MDE, MDD, MDA and other MD approaches?     

A software engineering perspective on environmental modeling framework design: The Object Modeling System

The environmental modeling community has historically been concerned with the proliferation of models and the effort associated with collective model development tasks (e.g., code generation, data transformation, etc.). Environmental modeling frameworks (EMFs) have been developed to address this problem, but much work remains before EMFs are adopted as mainstream modeling tools. Environmental model development requires both scientific understanding of environmental phenomena and software developer proficiency. EMFs support the modeling process through streamlining model code development, allowing seamless access to data, and supporting data analysis and visualization. EMFs also support aggregation of model components into functional units, component interaction and communication, temporal-spatial stepping, scaling of spatial data, multi-threading/multi-processor support, and cross-language interoperability. Some EMFs additionally focus on high-performance computing and are tailored for particular modeling domains such as ecosystem, socio-economic, or climate change research. The Object Modeling System Version 3 (OMS3) EMF employs new advances in software framework design to better support the environmental model development process. This paper discusses key EMF design goals/constraints and addresses software engineering aspects that have made OMS3 framework development efficacious and its application practical, as demonstrated by leveraging software engineering efforts outside of the modeling community and lessons learned from over a decade of EMF development. Software engineering approaches employed in OMS3 are highlighted including a non-invasive lightweight framework design supporting component-based model development, use of implicit parallelism in system design, use of domain specific language design patterns, and cloud-based support for computational scalability. The key advancements in EMF design presented herein may be applicable and beneficial for other EMF developers seeking to better support environmental model development through improved framework design.     

TOTEM: Reconciling multi-level modelling with standard two-level modelling

Model driven Engineering (MDE) advocates the active use of models throughout the different software development phases. In MDE, models are described using meta-models, one meta-level above. This approach effectively leaves developers with one single meta-level to create their models. However, there are scenarios where the use of multiple meta-levels results in simpler models with less accidental complexity. Hence, to simplify modelling in these cases, several multi-level modelling approaches and tools have recently emerged to increase the flexibility in modelling. While they provide advanced primitives to simplify modelling, there are possibilities to improve interoperability with mainstream two-level modelling approaches based on the Meta-Object Facility (MOF) standard of the Object Management Group (OMG), and achieve wider adoption.For this purpose, we first characterise the design space of multi-level modelling approaches using a feature model. On such a basis, we provide a detailed comparison of existing multi-level modelling tools, identifying gaps and research opportunities. As a result of this gap analysis, we propose a new approach to multi-level modelling that embeds multiple meta-levels within one meta-model (i.e., encoding objects as classes, and instantiation as inheritance), and a tool – called TOTEM – which implements these concepts. The tool capabilities and its benefits in terms of interoperability with mainstream, standard modelling frameworks are illustrated through an example, as well as with empirical and analytical evaluations.     

TALISMAN MDE: Mixing MDE principles

The Model-Driven Engineering approach is progressively gaining popularity in the software engineering community as it raises the level of abstraction in software development. In TALISMAN MDE framework, we combine the principles of the two most important initiatives, Model-Driven Architecture and Software Factories. Both have their pros and cons, and we select the best from each in TALISMAN MDE. To show the advantages of TALISMAN MDE, we have developed a systems generator and used it to create applications for controlling food traceability. The applications are being used in dairies with different manufacturing processes, using software developed specifically for each dairy by working only with models, without additional programming.     

Toward self-describing and workflow integrated Earth system models: A coupled atmosphere-ocean modeling system application

The complexity of Earth system models and their applications is increasing as a consequence of scientific advances, user demand, and the ongoing development of computing platforms, storage systems and distributed high-resolution observation networks. Multi-component Earth system models need to be redesigned to make interactions among model components and other applications external to the modeling system easier. To that end, the common component interfaces of Earth system models can be redesigned to increase interoperability between models and other applications such as various web services, data portals and science gateways. The models can be made self-describing so that the many configuration, build options and inputs of a simulation can be recorded. In this paper, we present a coupled modeling system that includes the proposed methodology to create self-describing models with common model component interfaces. The designed coupled atmosphere-ocean modeling system is also integrated into a scientific workflow system to simplify routine modeling tasks and relationships between these tasks and to demonstrate the enhanced interoperability between different technologies and components. Later on, the work environment is tested using a realistic Earth system modeling application. As can be seen through this example, a layered design for collecting provenance and metadata has the added benefit of documenting a run in far greater detail than before. In this way, it facilitates exploration and understanding of simulations and leads to possible reproducibility. In addition to designing self-describing Earth system models, the regular modeling tasks are also simplified and automated by using a scientific workflow which provides meaningful abstractions for the model, computing environment and provenance/metadata collection mechanisms. Our aim here is to solve a specific instance of a complex model integration problem by using a framework and scientific workflow approach together. The reader may also note that the methods presented in this paper might be also generalized to other types of Earth system models, leading to improved ease of use and flexibility. The initial results also show that the coupled atmosphere-ocean model, which is controlled by the designed workflow environment, is able to reproduce the Mediterranean Sea surface temperature when it is compared with the used CCSM3 initial and boundary conditions.     

Applying MDE to the (semi-)automatic development of model transformations

ContextModel transformations play a key role in any software development project based on Model-Driven Engineering principles. However, despite the inherent complexity of developing model transformations, little attention has been paid to the application of MDE principles to the development of model transformations.ObjectiveIn order to: (a) address the inherent complexity of model transformation development and (b) alleviate the problem of the diversity of the languages that are available for model transformation, this paper proposes the application of MDE principles to the development of model transformations. In particular, we have adopted the idea of handling model transformations as transformation models in order to be able to model, transform and generate model transformations.MethodThe proposal follows an MDA-based approach that entails the modeling of model transformations at different abstraction levels and the connection of these models by means of model transformations. It has been empirically validated by conducting a set of case studies following a systematic research methodology.ResultsThe proposal was supported by the introduction of MeTAGeM, a methodological and technical framework for the model-driven development of model transformations that bundles a set of Domain-Specific Languages for modeling model transformations with a set of model transformations in order to bridge these languages and (semi-)automate model transformations development.ConclusionThis paper serves to show that a semi-automatic development process for model transformations is not only desirable but feasible. This process, based on MDE principles, helps to ease the task of developing model transformations and to alleviate interoperability issues between model transformation languages.     

Gauss: A Framework for Verifying Scientific Computing Software

High performance scientific computing software is of critical international importance as it supports scientific explorations and engineering. Software development in this area is highly challenging owing to the use of parallel/distributed programming methods and complex communication and synchronization libraries. There is very little use of formal methods to debug software in this area, given that the scientific computing community and the formal methods community have not traditionally worked together. The Utah Gauss project combines expertise from scientific computing and formal methods in addressing this problem. We currently focus on MPI programs which are the kind that run on over 60% of world's supercomputers. These are programs written in C / C++ / FORTRAN employing message passing concurrency supported by the Message Passing Interface (MPI) library. Large-scale MPI programs also employ shared memory threads to manage concurrency within smaller task sub-groups, capitalizing on the recent availability of small-scale (e.g. single-chip) shared memory multiprocessors; such mixed programming styles can result in additional bugs. MPI libraries themselves can be buggy as they strive to implement complex requirements employing aggressive techniques such as multi-threading. We have built a model extractor that extracts from MPI C programs a formal model consisting of communicating processes represented in Microsoft's Zing modeling language. MPI library functions are also being modeled in Zing. This allows us to run formal analysis on the models to detect bugs in the MPI programs being analyzed. Our preliminary results and future plans are described; in addition, our contribution is to expose the special needs of this area and suggest specific avenues for problem- driven advances in software model-checking applied to scientific computing software development and verification.     

Where does model-driven engineering help? Experiences from three industrial cases

There have been few experience reports from industry on how Model-Driven Engineering (MDE) is applied and what the benefits are. This paper summarizes the experiences of three large industrial participants in a European research project with the objective of developing techniques and tools for applying MDE on the development of large and complex software systems. The participants had varying degrees of previous experience with MDE. They found MDE to be particularly useful for providing abstractions of complex systems at multiple levels or from different viewpoints, for the development of domain-specific models that facilitate communication with non-technical experts, for the purposes of simulation and testing, and for the consumption of models for analysis, such as performance-related decision support and system design improvements. From the industrial perspective, a methodology is considered to be useful and cost-efficient if it is possible to reuse solutions in multiple projects or products. However, developing reusable solutions required extra effort and sometimes had a negative impact on the performance of tools. While the companies identified several benefits of MDE, merging different tools with one another in a seamless development environment required several transformations, which increased the required implementation effort and complexity. Additionally, user-friendliness of tools and the provision of features for managing models of complex systems were identified as crucial for a wider industrial adoption of MDE.     

Secure System Modeling: Integrating Security Attacks with Statecharts

Software security is becoming an important concern as software applications are increasingly depending on the Internet, an untrustworthy computing environment. Vulnerabilities due to design errors, inconsistencies, incompleteness, and missing constraints in software design can be wrongly exploited by security attacks. Software functionality and security, however, are often handled separately in the development process. Software is designed with the mindset of its functionalities and cost, where the focus is mainly on the operational behavior. Security concerns, on the other hand, are often described in an imprecise way and open to subjective interpretations. This paper presents a threat driven approach that improves on the quality of software through the realization of a more secure model. The approach introduces systematic transformation rules and integration steps for integrating attack tree representations into statechart-based functional models. Through the focus on the behavior of an attack from the perspective of the system behavior, software engineers can clearly define and understand security concerns as software is designed. Security analysis and threat identification are then applied to the integrated model in order to identify and mitigate vulnerabilities at the design level.     

High-performance Earth system modeling with NASA/GSFC’s Land Information System

The Land Information System software (LIS; http://lis.gsfc.nasa.gov/, 2006) has been developed to support high-performance land surface modeling and data assimilation. LIS integrates parallel and distributed computing technologies with modern land surface modeling capabilities, and establishes a framework for easy interchange of subcomponents, such as land surface physics, input/output conventions, and data assimilation routines. The software includes multiple land surface models that can be run as a multi-model ensemble on global or regional domains with horizontal resolutions ranging from 2.5° to 1 km. The software may execute serially or in parallel on various high-performance computing platforms. In addition, the software has well-defined, standard-conforming interfaces and data structures to interface and interoperate with other Earth system models. Developed with the support of an Earth science technology office (ESTO) computational technologies project round~3 cooperative agreement, LIS has helped advance NASA’s Earth–Sun division’s software engineering principles and practices, while promoting portability, interoperability, and scalability for Earth system modeling. LIS was selected as a co-winner of NASA’s 2005 software of the year award.     

Assessing Software Quality Using the Markov Decision Processes

Quality of software is one of the most critical concerns in software system development, and many products fail to meet the quality objectives when constructed initially. Software quality is highly affected by the development process's actual dynamics. This article proposes the use of the Markov decision process (MDP) for the assessment of software quality because MDP is a useful technique to abstract the model of dynamics of the development process and to test its impact on quality. Additionally, the MDP modeling of the dynamics leads to early prediction of the quality, from the design phases all the way through the different stages of development. The proposed approach is based on the stochastic nature of the software development process, including project architecture, construction strategy of Software Quality Assurance system, its qualification actions, and team assignment strategy. It accepts these factors as inputs, generating a relative quality degree as an output. The proposed approach has been demonstrated for the design phase with a case study taken from the literature. The results prove its robustness and capability to identify appropriate policies in terms of quality, cost, and time. © 2011 Wiley Periodicals, Inc.     

Guest Editors' Introduction: Social Computing

Broadly stated, social computing takes a computational approach to the study and modeling of social interactions and communications. It also encompasses the development of technologies supporting these interactions. In recent years, we've seen social computing impact numerous information and communications technology (ICT) fields. It's attracted significant interest from not only researchers in the computing and social sciences but also software and online game vendors, Web entrepreneurs, political analysts, and digital-government practitioners, among others. This special issue samples the state of the art social-computing research from several perspectives: the overall paradigm of social-computing research; technological support for social-computing applications; cognitive modeling and architecture of agents and agent societies; and social-computing applications in areas such as terrorist network analysis, competitive business strategies, and agent behavior in financial markets. This article is part of a special issue on social computing.     

Design and implementations of Ninf: towards a global computing infrastructure

The world-wide computing infrastructure on the growing computer network technology is a leading technology to make a variety of information services accessible through the Internet for every user from the high-performance computing users through many of personal computing users. The important feature of such services is location transparency; information can be obtained irrespective of time or location in virtually shared manner. In this article, we overview Ninf, an ongoing global network-wide computing infrastructure project which allows users to access computational resources including hardware, software and scientific data distributed across a wide area network. Preliminary performance result on measuring software and network overhead is shown, and that promises the future reality of world-wide network computing.     

An experimental parallel system (EPS)

This paper reports on the initial stages of a research project involving the development of an experimental parallel computing system. The system is intended to support research in a variety of areas, including computer architectures, task models, language implementations and interconnection techniques. A pragmatic approach is being undertaken to evaluating techniques in these areas through applying the system to actual applications.

The system is based on a hierarchical structure of processors, using shared memory as the communication medium. This paper identifies the main features of the hardware being used, and presents an outline of the initial software for task creation and management.     

Reliable yet flexible software through formal model transformation (rule definition)

The results of literature review show that the need for both reliability and flexibility is increasingly becoming important among the various classes of software applications. Developing reliable yet flexible software is a hard problem. Although modeling methods enjoy a lot of advantages, the use of just one of them, in many cases, may not guarantee the development of reliable and flexible software. Formal modeling methods ensure reliability. However, lack of knowledge and high cost practically force developers to use semi-formal methods instead. Semi-formal (visual) modeling methods, which are widely used in practical large-scale software development, are not good enough for reliable software development. This paper proposes a new practical approach to the development of reliable yet flexible software. In the proposed approach, formal (Object-Z) and semi-formal (UML) models are transformed into each other using a set of bidirectional formal rules. Formal modeling and refinement ensure the reliability of software. Visual models facilitate the interactions among stakeholders who are not familiar enough with the complex mathematical concepts of formal methods. Visual models help detect the unexpected behavior and inconsistencies of software. Applying design patterns to visual models improves the flexibility of software. The transformation of formal and visual models into each other through the iterative and evolutionary process, proposed in this paper, helps develop the software applications that need to be highly reliable yet flexible. The feasibility of the proposed approach is evaluated using the multi-lift case study.     

A formalisation of the copy-modify-merge approach to version control in MDE

Models are the primary artefacts of the software development process in Model-Driven Engineering (MDE). Like other software artefacts, models undergo a complex evolution during their life cycles. Version control is one of the key techniques which enable developers to tackle this complexity. Traditional version control systems (VCS) are based on the copy-modify-merge approach which is not fully exploited in MDE since current implementations lack model-orientation. In this paper we provide a formalisation of the copy-modify-merge approach in the context of MDE. In particular, we analyse how the identification of commonalities and the calculation of differences can be defined by means of category-theoretical constructions. Moreover, we demonstrate how the properties of these constructions can be used to synchronise models and detect conflicting modifications.     

基于容器技术的水文水动力模型软硬件适配方法

随着国产化软硬件系统的发展和普及,将现行的计算程序适配到国产硬件和操作系统上是科学研究和业务化应用的关键,亟待探索提出专业计算模型的软硬件适配方法。现有关于专业计算模型的软硬件适配方法存在缺乏通用性、硬件依赖性强等问题。鉴于此,系统解析了国产化适配需要解决的关键问题,并对比了现行的软件适配技术,筛选出容器技术作为水文水动力模型的国产适配技术。容器技术可将应用程序打包成独立的运行环境,摆脱对底层架构和操作系统的依赖。以水文水动力模型TELEMAC为例,详细说明了Docker镜像构成原理,并通过Dockerfile文件构建了TELEMAC镜像环境,开展了计算案例的验证。结果表明TELEMAC镜像能够安全运行在以鲲鹏920处理器为核心的openEuler和麒麟V10等国产软硬件平台上,且案例计算结果与标准结果相一致,模型计算效率高,实现了专业科学计算模型的国产化软硬件适配,该研究可为其他软件国产化适配提供参考借鉴。