Search

This document is a guest editorial for the special section on SEFM 2020 and 2021 in the journal Software & Systems Modeling. The International Conference on Software Engineering and Formal Methods (SEFM) aims to bring together practitioners and researchers to advance the state of the art in formal methods and their application in the software industry. This special section includes selected papers from SEFM 2020 and 2021, which were held virtually during the COVID pandemic. Each article in this section has undergone rigorous peer review and has been revised and extended compared to its conference version. The selected papers cover topics such as embedded software portability and verification, nontermination inference, quantitative modeling and analysis of BDI agents, lazy model checking for recursive state machines, P-stable abstractions of hybrid systems, fairness and guarantees for extended bounded response LTL+P synthesis, counterexample classification, analyzing the impact of human errors on interactive service robotic scenarios, and active model learning of stochastic reactive systems. [Extracted from the article]

This document is a guest editorial for a special section in the journal "Software & Systems Modeling." The special section features revised and extended versions of selected papers from the 20th International Conference on Software Engineering and Formal Methods (SEFM'22), which was held in Berlin, Germany in September 2022. The SEFM conference series aims to advance the state of the art in formal methods and their integration into practical software engineering methods and tools. The special section includes papers on topics such as user-centric analysis, automated generation of finite automata, formal specifications of smart contracts, distributed verification of programs, and abstraction-based verification of neural networks. The authors express their gratitude to the authors and reviewers for their contributions and thank Springer for their support in publishing the special section. [Extracted from the article]

Models are a universal instrument in science, technology, and daily life. They function as instruments in almost every scenario. Any human activity can be (and is) supported by models, e.g. reason, explain, design, act, predict, explore, communicate, collaborate, interact, orient, direct, guide, socialises, perceive, reflect, develop, making sense, teach, learn, imagine, etc. This universal suitability is also the basis for a wide use of models and modelling in Computer Science and Engineering. We claim that models form the fourth dimension in Computer Science. This paper sketches and systematises the main ingredients of the study model and modelling. [ABSTRACT FROM AUTHOR]

The article presents an overview of the research papers which were presented during the 2003 Unified Modelling Language conference. A systematic way of designing interactions by stepwise refinement was developed. One paper describes a snapshot sequence language which has been implemented to help designers to make better use of complex snapshots of a given model. One paper describes the author's experiences with a tool called Netsilon which has been developed to apply the model-driven engineering approach to web applications.

Aspect-Oriented Modeling (AOM) techniques allow software designers to isolate and address separately solutions for crosscutting concerns (such as security, reliability, new functional features, etc.). Current AOM research is concerned not only with the separate expression of concerns and their composition into a complete system model, but also with the analysis of different properties of such models. This paper proposes an approach for analyzing the performance effects of a given aspect on the overall system performance, after the composition of the aspect model with the system’s primary model. Performance analysis of UML models is enabled by the “UML Performance Profile for Schedulability, Performance and Time” (SPT) standardized by OMG, which defines a set of quantitative performance annotations to be added to a UML model. The first step of the proposed approach is to add performance annotations to both the primary and the aspect models. An aspect model is generic at first, and therefore its performance annotations must be parameterized. A generic model is converted into a context-specific aspect model with concrete values assigned to its performance annotations. The latter is composed with the primary model, generating a complete annotated UML model. The composition is performed in both structural and behavioural views. A novel approach for composing activity diagrams based on graph-rewriting concepts is proposed in the paper. The next step is to transform automatically the composed model into a Layered Queueing Network (LQN) performance model, by using techniques developed in previous work. The proposed approach is illustrated with a case study system, whose primary model is enhanced with some security features by using AOM. The performance effects of the security aspect under consideration are analyzed in two design alternatives, by solving and analyzing the LQN model of the composed system. [ABSTRACT FROM AUTHOR]

We understand this paper as a contribution to the "anatomy" of conceptual models. We propose a signature of conceptual models for their characterization, which allows a clear distinction from other types of models. The motivation for this work arose from the observation that conceptual models are widely discussed in science and practice, especially in computer science, but that their potential is far from being exploited. We combine our proposal of a more transparent explanation of the nature of conceptual models with an approach that classifies conceptual models as a link between the dimension of linguistic terms and the encyclopedic dimension of notions. As a paradigm we use the triptych, whose central tableau represents the model dimension. The effectiveness of this explanatory approach is illustrated by a number of examples. We derive a number of open research questions that should be answered to complete the anatomy of conceptual models. [ABSTRACT FROM AUTHOR]

Object-Oriented Information System (OOIS) is an information system that employs object-oriented technologies in system design and implementation. Recent research advances and industrial innovations in distributed system modeling and Internet applications have enabled OOIS design and implementation to be carried out on the basis of new technologies and platforms. This special section onModeling Object-Oriented Information Systemspresents readers with a set of best papers selected from the 7th International Conference on OOIS. Reviews of theories and applications of OOIS’s are also provided for predicating trends in OOIS modeling. [ABSTRACT FROM AUTHOR]

Automatic generation of textual artefacts (including code, documentation, configuration files, build scripts, etc.) from models in a software development process through the application of model-to-text (M2T) transformation is a common MDE activity. Despite the importance of M2T transformation, contemporary M2T languages lack support for developing transformations that scale with the size of the input model. As MDE is applied to systems of increasing size and complexity, a lack of scalability in M2T transformation languages hinders industrial adoption. In this paper, we propose a form of runtime analysis that can be used to identify the impact of source model changes on generated textual artefacts. The structures produced by this runtime analysis, property access traces, can be used to perform efficient source-incremental transformation: our experiments show an average reduction of 60% in transformation execution time compared to non-incremental (batch) transformation. [ABSTRACT FROM AUTHOR]

Event-based communication is used in different domains including telecommunications, transportation, and business information systems to build scalable distributed systems. Such systems typically have stringent requirements for performance and scalability as they provide business and mission critical services. While the use of event-based communication enables loosely-coupled interactions between components and leads to improved system scalability, it makes it much harder for developers to estimate the system's behavior and performance under load due to the decoupling of components and control flow. In this paper, we present our approach enabling the modeling and performance prediction of event-based systems at the architecture level. Applying a model-to-model transformation, our approach integrates platform-specific performance influences of the underlying middleware while enabling the use of different existing analytical and simulation-based prediction techniques. In summary, the contributions of this paper are: (1) the development of a meta-model for event-based communication at the architecture level, (2) a platform aware model-to-model transformation, and (3) a detailed evaluation of the applicability of our approach based on two representative real-world case studies. The results demonstrate the effectiveness, practicability and accuracy of the proposed modeling and prediction approach. [ABSTRACT FROM AUTHOR]

The goal of autonomic computing is to reduce the configuration, operational, and maintenance costs of distributed applications by enabling them to self-manage, self-heal, and self-optimize. This paper provides two contributions to the Model-Driven Engineering (MDE) of autonomic computing systems using Enterprise Java Beans (EJBs). First, we describe the structure and functionality of an MDE tool that visually captures the design of EJB applications, their quality of service (QoS) requirements, and the adaptations applied to their EJBs. Second, the paper describes how MDE tools can be used to generate code to simulate adaptive systems for verification and plug EJBs into a Java component framework that provides runtime adaptation capabilities. [ABSTRACT FROM AUTHOR]

CSP || B is a formal approach which combines state and event-based descriptions of a system. It enables the automatic verification of dynamic properties using model checking techniques. In this paper we identify a variation on the standard CSP || B architecture so that it is more applicable to support the specification of information systems. We specify a library system using this new architecture. We examine several safety and liveness requirements and demonstrate that we can compositionally verify them using FDR. If a property fails to model check we identify an abstraction technique which enables us to pinpoint the cause of the failure. [ABSTRACT FROM AUTHOR]

This discussion paper refers to the article “Matters on (Meta-)Modeling” of Thomas Kühne. Many of his concepts and proposals are appreciated, as e.g. the clear distinction of type and token models or of prominent relationships like instantiation, generalisation or “meta-ness”. However, for some of the presented views and definitions alternative approaches may be followed. This concerns e.g. the relationship between models and their originals (“systems”) including the distinction of descriptive and prescriptive models, the view on various kinds of instantiation and the way how metamodels are defined. Some of these questions are debated in detail and alternative positions are presented. [ABSTRACT FROM AUTHOR]

This paper presents Reconciliation+, a method which identifies overlaps between models of software systems behaviour expressed as UML object interaction diagrams (i.e., sequence and/or collaboration diagrams), checks whether the overlapping elements of these models satisfy specific consistency rules and, in cases where they violate these rules, guides software designers in handling the detected inconsistencies. The method detects overlaps between object interaction diagrams by using a probabilistic message matching algorithm that has been developed for this purpose. The guidance to software designers on when to check for inconsistencies and how to deal with them is delivered by enacting a built-in process model that specifies the consistency rules that can be checked against overlapping models and different ways of handling violations of these rules. Reconciliation+ is supported by a toolkit. It has also been evaluated in a case study. This case study has produced positive results which are discussed in the paper. [ABSTRACT FROM AUTHOR]

Model Driven Architecture (MDA) is an approach to application modeling and generation that has received a lot of attention in recent months. Championed by the Object Management Group (OMG), many organizations are now looking at the ideas of MDA as a way to organize and manage their application solutions, tool vendors are explicitly referring to their capabilities in terms of “MDA compliance”, and the MDA lexicon of platform-specific and platform-independent models is now widely referenced in the industry.In spite of this interest and market support, there is little clear guidance on what MDA means, where we are in its evolution, what is possible with today’s technology, and how to take advantage of it in practice. This paper addresses that need by providing an analysis of how modeling is used in industry today, the relevance of MDA to today’s systems, a classification of MDA tooling support, and examples of its use. The paper concludes with a set of recommendations for how MDA can be successful in practice. [ABSTRACT FROM AUTHOR]

To predict the performance of an application, it is crucial to consider the performance of the underlying infrastructure. Thus, to yield accurate prediction results, performance-relevant properties and behaviour of the infrastructure have to be integrated into performance models. However, capturing these properties is a cumbersome and error-prone task, as it requires carefully engineered measurements and experiments. Existing approaches for creating infrastructure performance models require manual coding of these experiments, or ignore the detailed properties in the models. The contribution of this paper is the Goal-oriented INfrastructure Performance EXperiments ( Ginpex) approach, which introduces goal-oriented and model-based specification and generation of executable performance experiments for automatically detecting and quantifying performance-relevant infrastructure properties. Ginpex provides a metamodel for experiment specification and comes with predefined experiment templates that provide automated experiment execution on the target platform and also automate the evaluation of the experiment results. We evaluate Ginpex using three case studies, where experiments are executed to quantify various infrastructure properties. [ABSTRACT FROM AUTHOR]

Model composition plays a central role in many software engineering activities, e.g., evolving design models to add new features. To support these activities, developers usually rely on model composition heuristics. The problem is that the models to-be-composed usually conflict with each other in several ways and such composition heuristics might be unable to properly deal with all emerging conflicts. Hence, the composed model may bear some syntactic and semantic inconsistencies that should be resolved. As a result, the production of the intended model is an error-prone and effort-consuming task. It is often the case that developers end up examining all parts of the output composed model instead of prioritizing the most critical ones, i.e., those that are likely to be inconsistent with the intended model. Unfortunately, little is known about indicators that help developers (1) to identify which model is more likely to exhibit inconsistencies, and (2) to understand which composed models require more effort to be invested. It is often claimed that software systems remaining stable over time tends to have a lower number of defects and require less effort to be fixed than unstable systems. However, little is known about the effects of software stability in the context of model evolution when supported by composition heuristics. This paper, therefore, presents an exploratory study analyzing stability as an indicator of inconsistency rate and resolution effort on model composition activities. Our findings are derived from 180 compositions performed to evolve design models of three software product lines. Our initial results, supported by statistical tests, also indicate which types of changes led to lower inconsistency rate and lower resolution effort. [ABSTRACT FROM AUTHOR]

The accuracy of performance-prediction models is crucial for widespread adoption of performance prediction in industry. One of the essential accuracy-influencing aspects of software systems is the dependence of system behaviour on a configuration, context or history related state of the system, typically reflected with a (persistent) system attribute. Even in the domain of component-based software engineering, the presence of state-reflecting attributes (the so-called internal states) is a natural ingredient of the systems, implying the existence of stateful services, stateful components and stateful systems as such. Currently, there is no consensus on the definition or method to include state-related information in component-based prediction models. Besides the task to identify and localise different types of stateful information across component-based software architecture, the issue is to balance the expressiveness and complexity of prediction models via an effective abstraction of state modelling. In this paper, we identify and classify stateful information in component-based software systems, study the performance impact of the individual state categories, and discuss the costs of their modelling in terms of the increased model size. The observations are formulated into a set of heuristics-guiding software engineers in state modelling. Finally, practical effect of state modelling on software performance is evaluated on a real-world case study, the SPECjms2007 Benchmark. The observed deviation of measurements and predictions was significantly decreased by more precise models of stateful dependencies. [ABSTRACT FROM AUTHOR]

Interval logics formalize temporal reasoning on interval structures over linearly (or partially) ordered domains, where time intervals are the primitive ontological entities and truth of formulae is defined relative to time intervals, rather than time points. In this paper, we introduce and study Metric Propositional Neighborhood Logic (MPNL) over natural numbers. MPNL features two modalities referring, respectively, to an interval that is 'met by' the current one and to an interval that 'meets' the current one, plus an infinite set of length constraints, regarded as atomic propositions, to constrain the length of intervals. We argue that MPNL can be successfully used in different areas of computer science to combine qualitative and quantitative interval temporal reasoning, thus providing a viable alternative to well-established logical frameworks such as Duration Calculus. We show that MPNL is decidable in double exponential time and expressively complete with respect to a well-defined sub-fragment of the two-variable fragment $${{\rm FO}^2[\mathbb{N},=,<,s]}$$ of first-order logic for linear orders with successor function, interpreted over natural numbers. Moreover, we show that MPNL can be extended in a natural way to cover full $${{\rm FO}^2[\mathbb{N},=,<,s]}$$, but, unexpectedly, the latter (and hence the former) turns out to be undecidable. [ABSTRACT FROM AUTHOR]

Where object-oriented languages deal with objects as described by classes, model-driven development uses models, as graphs of interconnected objects, described by metamodels. A number of new languages have been and continue to be developed for this model-based paradigm, both for model transformation and for general programming using models. Many of these use single-object approaches to typing, derived from solutions found in object-oriented systems, while others use metamodels as model types, but without a clear notion of polymorphism. Both of these approaches lead to brittle and overly restrictive reuse characteristics. In this paper we propose a simple extension to object-oriented typing to better cater for a model-oriented context, including a simple strategy for typing models as a collection of interconnected objects. We suggest extensions to existing type system formalisms to support these concepts and their manipulation. Using a simple example we show how this extended approach permits more flexible reuse, while preserving type safety. [ABSTRACT FROM AUTHOR]

State machines, represented by statecharts or state machine diagrams, are an important formalism for behavioural modelling. According to the research literature, the most popular statechart formalisms appear to be Classical, UML, and that implemented by R hapsody. These three formalisms seem to be very similar; however, there are several key syntactic and semantic differences. These differences are enough that a model written in one formalism could be ill-formed in another formalism. Worse, a model from one formalism might actually be well-formed in another, but be interpreted differently due to the semantic differences. This paper summarizes the results of an informal comparative study of these three formalisms with the help of several illustrative examples. We present a classification of the differences according to the nature of potential problems caused by each difference. In addition, for each difference we discuss how translation between formalisms can be achieved, if at all. [ABSTRACT FROM AUTHOR]

The timed UML and RT-LOTOS environment, or TURTLE for short, extends UML class and activity diagrams with composition and temporal operators. TURTLE is a real-time UML profile with a formal semantics expressed in RT-LOTOS. Further, it is supported by a formal validation toolkit. This paper introduces TURTLE-P, an extended profile no longer restricted to the abstract modeling of distributed systems. Indeed, TURTLE-P addresses the concrete descriptions of communication architectures, including quality of service parameters (delay, jitter, etc.). This new profile enables co-design of hardware and software components with extended UML component and deployment diagrams. Properties of these diagrams can be evaluated and/or validated thanks to the formal semantics given in RT-LOTOS. The application of TURTLE-P is illustrated with a telecommunication satellite system. [ABSTRACT FROM AUTHOR]

In this contribution, it is shown that perfect synchroneous specifications can be partitioned to and implemented on a distributed processor network. To this end, we introduce a lean visual formalism, called μ-charts, that is similar to the specification language Statecharts. This formalism consists of fewer syntactic constructs than Statecharts. Further syntax like hierarchical decomposition can be derived by means of syntactic abbreviation. μ-charts' semantics is based on the assumption of perfect synchrony. This paper is one of several contributions in this context; it gives a formal background and concentrates on the question how to use perfect synchroneous, state-based description techniques as a basis for distributed implementations. The main contribution presented in this article is that the (formal and compositional) semantics of a perfect synchroneous specification is preserved when it is partitioned and implemented on distributed processors. We prove a theorem which guarantees that the communication flow between distributed parts of a perfect synchroneous specification stabilizes in a fixed point, i.e.$ terminates, independently of the processor speeds. [ABSTRACT FROM AUTHOR]

The paper presents STAIRS [1], an approach to the compositional development of UML interactions supporting the specification of mandatory as well as potential behavior. STAIRS has been designed to facilitate the use of interactions for requirement capture as well as test specification. STAIRS assigns a precise interpretation to the various steps in incremental system development based on an approach to refinement known from the field of formal methods and provides thereby a foundation for compositional analysis. An interaction may characterize three main kinds of traces. A trace may be (1) positive in the sense that it is valid, legal or desirable, (2) negative meaning that it is invalid, illegal or undesirable, or (3) inconclusive meaning that it is considered irrelevant for the interaction in question. The basic increments in system development proposed by STAIRS, are structured into three main kinds referred to as supplementing, narrowing and detailing. Supplementing categorizes inconclusive traces as either positive or negative. Narrowing reduces the set of positive traces to capture new design decisions or to match the problem more adequately. Detailing involves introducing a more detailed description without significantly altering the externally observable behavior. [ABSTRACT FROM AUTHOR]

A rule-based update transformation is a model transformation where a single model is transformed in place. A model refactoring is a model transformation that improves the design described in the model. A refactoring should only affect a previously chosen subset of the original model. In this paper, we discuss how to define and execute model refactorings as rule-based transformations in the context of the UML and MOF standards. We also present an experimental tool to execute this kind of transformation. [ABSTRACT FROM AUTHOR]

A major purpose of analysis is to represent precisely all relevant facts, as they are observed in the external world. A substantial problem in object-oriented analysis is that most modelling languages are more suitable to build computational models than to develop conceptual models. It is a rather blind assumption that concepts that are convenient for design can also be applied during analysis. Preconditions, postconditions and invariants are typical examples of concepts with blurred semantics. At the level of analysis they are most often used to specify business rules. This paper introduces proper concepts for modelling business rules and specifies their semantics. [ABSTRACT FROM AUTHOR]

Integrating software components to produce large-scale software systems is an effective way to reuse experience and reduce cost. However, unexpected interactions among components when integrated into software systems are often the cause of failures. Discovering these composition errors early in the development process could lower the cost and effort in fixing them. This paper introduces a rigorous analysis approach to software design composition based on automated verification techniques. We show how to represent, instantiate and integrate design components, and how to find design composition errors using model checking techniques. We illustrate our approach with a Web-based hypermedia case study. [ABSTRACT FROM AUTHOR]

How should the World Wide Web look like if it were for location-based information? And how would mobile, spatially aware applications deal with such a platform? In this paper we present theneXusAugmented World Model, an object oriented data model which plays a major role in an open framework for both providers of location-based information and new kinds of applications: theneXusplatform. We illustrate the usability of the model with several sample applications and show the extensibility of this framework. At last we present a stepwise approach for building spatially aware applications in this environment. [ABSTRACT FROM AUTHOR]

We show that Span (Graph) ∗ , an algebra for open transition systems introduced by Katis, Sabadini and Walters, satisfies a universal property. By itself, this is a justification of the canonicity of this model of concurrency. However, the universal property is itself of interest, being a formal demonstration of the relationship between feedback and state. Indeed, feedback categories, also originally proposed by Katis, Sabadini and Walters, are a weakening of traced monoidal categories, with various applications in computer science. A state bootstrapping technique, which has appeared in several different contexts, yields free such categories. We show that Span (Graph) ∗ arises in this way, being the free feedback category over Span (Set) . Given that the latter can be seen as an algebra of predicates, the algebra of open transition systems thus arises—roughly speaking—as the result of bootstrapping state to that algebra. Finally, we generalize feedback categories endowing state spaces with extra structure: this extends the framework from mere transition systems to automata with initial and final states. [ABSTRACT FROM AUTHOR]

Many software development, planning, or analysis tasks require an up-to-date software architecture documentation. However, this documentation is often outdated, unavailable, or at least not available as a formal model which analysis tools could use. Reverse engineering methods try to fill this gap. However, as they process the system's source code, they are easily misled by design deficiencies (e.g., violations of component encapsulation) which leaked into the code during the system's evolution. Despite the high impact of design deficiencies on the quality of the resulting software architecture models, none of the surveyed related works is able to cope with them during the reverse engineering process. Therefore, we have developed the Archimetrix approach which semiautomatically recovers the system's concrete architecture in a formal model while simultaneously detecting and removing design deficiencies. We have validated Archimetrix on a case study system and two implementation variants of the CoCoME benchmark system. Results show that the removal of relevant design deficiencies leads to an architecture model which more closely matches the system's conceptual architecture. [ABSTRACT FROM AUTHOR]

We describe a behavioural modelling approach based on the concept of a “Protocol Machine”, a machine whose behaviour is governed by rules that determine whether it accepts or refuses events that are presented to it. We show how these machines can be composed in the manner of mixins to model object behaviour and show how the approach provides a basis for defining reusable fine-grained behavioural abstractions. We suggest that this approach provides better encapsulation of object behaviour than traditional object modelling techniques when modelling transactional business systems. We relate the approach to work going on in model driven approaches, specifically the Model Driven Architecture initiative sponsored by the Object Management Group. [ABSTRACT FROM AUTHOR]

The impact of model-based design on the software engineering community is impressive, and recent research in model transformations, and elegant behavioral specifications of systems has the potential to revolutionize the way in which systems are designed. Such techniques aim to raise the level of abstraction at which systems are specified, to remove the burden of producing application-specific programs with general-purpose programming. For complex real-time systems, however, the impact of model-driven approaches is not nearly so widespread. In this paper, we present a perspective of model-based design researchers who joined with software experts in robotics to enter the DARPA Urban Challenge, and to what extent model-based design techniques were used. Further, we speculate on why, according to our experience and the testimonies of many teams, the full promises of model-based design were not widely realized for the competition. Finally, we present some thoughts for the future of model-based design in complex systems such as these, and what advancements in modeling are needed to motivate small-scale projects to use model-based design in these domains.

We present a controlled experiment for the empirical evaluation of example-driven modeling (EDM), an approach that systematically uses examples for model comprehension and domain knowledge transfer. We conducted the experiment with 26 graduate (Masters and Ph.D. level) and undergraduate (Bachelor level) students from electrical and computer engineering, computer science, and software engineering programs at the University of Waterloo. The experiment involves a domain model, with UML class diagrams representing the domain abstractions and UML object diagrams representing examples of using these abstractions. The goal is to provide empirical evidence of the effects of suitable examples on model comprehension, compared to having model abstractions only, by having the participants perform model comprehension tasks. Our results show that EDM is superior to having model abstractions only, with an improvement of 39% for diagram completeness, 33% for questions completeness, 71% for efficiency, and a reduction in the number of mistakes by 80%. We provide qualitative results showing that participants receiving model abstractions augmented with examples experienced lower perceived difficulty in performing the comprehension tasks, higher perceived confidence in their tasks' solutions, and asked 90% fewer clarifying domain questions. We also present participants' feedback regarding the usefulness of the provided examples, their number and types, as well as the use of partial examples. We present a taxonomy of the different types of examples, explain their significance, and propose guidelines for manual and automatic creation of useful examples. [ABSTRACT FROM AUTHOR]

This article discusses a model intelligence technique called proactive modeling. The goal of proactive modeling is to reduce the amount of manual modeling required when using a graphical DSML and to assist in step-by-step creation of a model. Proactive modeling accomplishes this goal by examining the metamodels syntax and constraints, automatically executing model modifications, and prompting the modeler for assistance when more than one valid model modification exists, but none are necessary. We have integrated proactive modeling into the generic modeling environment (GME) as a generic add-on that can operate on any domain-specific modeling language implemented in GME. Lastly, results from applying proactive modeling to several DSMLs in GME show that it can reduce modeling effort. [ABSTRACT FROM AUTHOR]

We present an approach to model-driven software product line engineering which is based on feature models and domain models. A feature model describes both common and varying properties of the instances of a software product line. The domain model is composed of a structural model (package and class diagrams) and a behavioral model (story diagrams). Features are mapped onto the domain model by annotating elements of the domain model with features. An element of a domain model is specific to the features included in its feature annotation. An instance of the product line is defined by a set of selected features (a feature configuration). A configuration of the domain model is built by excluding all elements whose feature set is not included in the feature configuration. To ensure consistency of the configured domain model, we define constraints on the annotations of inter-dependent domain model elements. These constraints guarantee that a model element may be selected only when the model elements are also included on which it depends. Violations of dependency constraints may be removed automatically with the help of an error repair tool which propagates features to dependent model elements. [ABSTRACT FROM AUTHOR]

Probabilistic models are commonly used to evaluate quality attributes, such as reliability, availability, safety and performance of software-intensive systems. The accuracy of the evaluation results depends on a number of system properties which have to be estimated, such as environmental factors or system usage. Researchers have tackled this problem by including uncertainties in the probabilistic models and solving them analytically or with simulations. The input parameters are commonly assumed to be normally distributed. Accordingly, reporting the mean and variances of the resulting attributes is usually considered sufficient. However, many of the uncertain factors do not follow normal distributions, and analytical methods to derive objective uncertainties become impractical with increasing complexity of the probabilistic models. In this work, we introduce a simulation-based approach which uses Discrete Time Markov Chains and probabilistic model checking to accommodate a diverse set of parameter range distributions. The number of simulation runs automatically regulates to the desired significance level and reports the desired percentiles of the values which ultimately characterises a specific quality attribute of the system. We include a case study which illustrates the flexibility of this approach using the evaluation of several probabilistic properties. [ABSTRACT FROM AUTHOR]

The author discusses the association between theoretical and applied information science and the concept of model. He highlights that the branch of science may be understood in various ways such as the scientific communities practicing it, its objects of study, and the methods and tools which it applies. The author emphasizes that information science models always play a dominant role regardless of the perspective from which information science is viewed.

In this article, we describe successive versions of a metamodeling language using a set-theoretic formalization. We focus on language extension mechanisms, particularly on the relatively new subset and union properties of MOF 2.0 and the UML 2.0 Infrastructure. We use Liskov substitutability as the rationale for our formalization. We also show that property redefinitions are not a safe language extension mechanism. Each language version provides new features, and we note how such features cannot be mixed arbitrarily. Instead, constraints over the metamodel and model structures must be established. We expect that this article provides a better understanding of the foundations of MOF 2.0, which is necessary to define new extensions, model transformation languages and tools. [ABSTRACT FROM AUTHOR]

Security requirements have become an integral part of most modern software systems. In order to produce secure systems, it is necessary to provide software engineers with the appropriate systematic support. We propose a methodology to integrate the specification of access control policies into Unified Modeling Language (UML) and provide a graph-based formal semantics for the UML access control specification which permits to reason about the coherence of the access control specification. The main concepts in the UML access control specification are illustrated with an example access control model for distributed object systems. [ABSTRACT FROM AUTHOR]

We study the testing and certification of UML and OCL models as supported by the validation tool USE. We extend the available USE features by introducing a language for defining properties of desired snapshots and by showing how such snapshots are generated. Within the approach, it is possible to treat test cases and validation cases. Test cases show that snapshots having desired properties can be constructed. Validation cases show that given properties are consequences of the original UML and OCL model. [ABSTRACT FROM AUTHOR]

Ontology can be considered as a comprehensive knowledge model which enables the developer to practice knowledge, instead of code, reuse. In the development of knowledge-based systems, different modeling languages are employed at different stages of the development process. By using a common modeling language for the knowledge and software models, knowledge instead of software reuse can be achieved. We illustrate the process by first presenting an ontology developed for an industrial domain and then investigate Unified Modeling Language (UML) as an ontology modeling tool. Since any model expressed in UML can be translated into a software model, the transition from the knowledge model to system implementation is better supported with the proposed approach. The industrial domain of selecting a remediation technique for petroleum contaminated sites is adopted for the illustration case study. [ABSTRACT FROM AUTHOR]