Abstract The graphical nature of prominent modelling notations, such as the standards UML and SysML, enables them to tap into the cognitive benefits of diagrams. However, these notations hardly exploit the cognitive potential of diagrams and are only partially graphical with invariants and operations being expressed textually. The Visual Contract Language (VCL) aims at improving visual modelling; it tries to (a) maximise diagrammatic cognitive effectiveness, (b) increase visual expressivity, and (c) level of rigour and formality. It is an alternative to UML that does largely pictorially what is traditionally done textually. The paper presents the results of a controlled experiment carried out four times in different academic settings and involving 43 participants, which compares VCL against UML and OCL and whose goal is to provide insight on benefits and limitations of visual modelling. The paper’s hypotheses are evaluated using a crossover design with the following tasks: (i) modelling of state space, invariants and operations, (ii) comprehension of modelled problem, (iii) detection of model defects and (iv) comprehension of a given model. Although visual approaches have been used and advocated for decades, this is the first empirical investigation looking into the effects of graphical expression of invariants and operations on modelling and model usage tasks. Results suggest VCL benefits in defect detection, model comprehension, and modelling of operations, providing some empirical evidence on the benefits of graphical software design.

In Model-Driven Engineering (MDE), models are the primary artifacts of software development life cycles. Being an abstraction of the real systems, models are generally believed to be less complex and better suited for developing, comprehending, communicating, and analyzing systems. However, such an advantage is decreasing with the tendency of models themselves getting more and more complex. In this paper we propose a model decomposition technique for reducing model size and consequently complexity by exploiting the notion of dependency graphs. Compared to its predecessor, this new model decomposition technique is more effective in terms of both the number of derived sub-models (more), the size of sub-models (finer), and the quality of sub-models (better). We demonstrate the improved effectiveness by applying both the previous and the new algorithm to a common example and comparing the results.

Model transformations play a key role in model driven software engineering approaches. Validation of model transformations is crucial for the quality assurance of software systems to be constructed. The relational logic based specification language Alloy and its accompanying tool the Alloy Analyzer have been used in the past to validate properties of model transformations. However Alloy based analysis of transformations suffers from time complexity and scalability issues. The problem becomes even more severe when it comes to higher order transformations that are inherently more complex. In previous work, we proposed a sub-language of Alloy, called F-Alloy, that is tailored for model transformation specifications. Instead of pure analysis based validation, F-Alloy speeds up the validation of model transformations by applying a hybrid strategy that combines analysis with interpretation. In this paper, we show how the F-Alloy approach can be extended to also support efficient validation of higher order transformations.

Modelling languages are defined by specifying their abstract syntax, concrete syntax and semantics. In the Lightning tool the definition of all these language components is based on the lightweight formal language Alloy. Lightning makes use of the powerful automatic analysis features of Alloy to allow language designers to develop and validate the definition of a modelling language in an incremental fashion. By providing immediate visual feedback, it allows errors in the language definition to be quickly identified and corrected. Furthermore Lightning introduces F-Alloy, a new Alloy based model transformation language. Transformations expressed in F-Alloy can be efficiently interpreted in Lightning. We illustrate the use of the tool on the language of structured business processes.

Verifying whether a business process is compliant with a regulatory framework is a difficult task. In the present paper we prove the hardness of the business process regulatory compliance problem by taking into account a sub-problem of the general problem. This limited problem allows to verify only the compliance of structured processes with respect to a regulatory framework composed of a set of conditional obligations including a deadline. Experimental evidence from existing studies shows that compliance is a difficult task. In this paper, despite considering a sub-problem of the general problem, we provide some theoretical evidence of the difficulty of the task. In particular we show that the source of the complexity lies in the core language of verifying conditional obligations with a deadline. We prove that for this simplified case verifying partial compliance belongs to the class of NP-complete problems, and verifying full compliance belongs to the class of coNP-complete problems. Thus by proving the difficulty of a simplified compliance problem we prove that the general problem of verifying business process regulatory compliance is hard.

Regulatory compliance management is now widely recognized as one of the main challenges still to be efficiently dealt with in information systems. In the discipline of business process management in particular, compliance is considered as an important driver of the efficiency, reliability and market value of companies. It consists of ensuring that enterprise systems behave according to some guidance provided in the form of regulations. This paper gives a definition of the research problem of regulatory compliance. We show why we expect a formal policy-based and model-driven approach to provide significant advantages in allowing enterprises to flexibly manage decision-making related to regulatory compliance. For this purpose, we contribute CoReL, a domain-specific modeling language for representing compliance requirements that has a graphical concrete syntax. Informal semantics of CoReL are introduced and its use is illustrated on an example. CoReL allows to leverage business process compliance modeling and checking, enhancing it with regard to, among other dimensions, user-friendliness, genericity, and traceability.

Visual representations are widely used to describe modern-day software systems, but, in most cases, they lack rigour. This paper addresses the problems of formality, rigour and complexity in visual descriptions of software systems. It proposes a new language, VCL, that is designed to be visual, formal and modular, and that targets abstract specification at the level of requirements. VCL aims at expressing visually structural and behavioural properties of software systems. This paper presents design of VCL, outlining syntax and semantics of VCL notations of structural, behavioural, constraint, and contract diagrams, together with VCL's approach to behavioural modelling based on design by contract. VCL's novelty lies in the fact that contracts are modular units.

SPLACID is a semi-formal language conceived for the specification and synthesis of (advanced) transactional models from basic features, such as transaction types and (relaxed) ACID variants. SPLACID is an improvement of the ACTA framework offering a well-structured and formal syntax. Neither ACTA nor SPLACID, however, benefit from a formal tool-supported semantics. This paper presents the first step for having a full formal semantics of SPLACID by translation to Alloy. In particular, we present the translation of the SPLACID concepts into Alloy concepts focusing on those concepts pertaining to the structure of a Transactional Model and those characterizing the isolation variant. The Alloy specification obtained by this translation preserve the SPLACID main key-properties, namely, modularity, flexibility and reusability. To support this claim we show how flexible, modular and reusable structures and isolation variants can be obtained in Alloy. Finally, we analyze the flat and nested transactional model structures and the serializability-based isolation variant using the Alloy Analyzer.

We present a new approach to executable modeling that borrows from executable UML the notion of domains and bridges and couches them in a formal abstract framework based on the novel concept of a domain hierarchy. The framework is independent of the language used for representing structure and behavior of domains and bridges. By plugging in a declarative executable modeling language with a formal semantics for representing both structure and behavior, we instantiate the abstract framework into a concrete framework that shares with executable UML the benefits of a high-level separation of the platform-independent model into domains and bridges while providing a formal and declarative description of the underlying models.

Let P be a property of undirected graphs. We consider the following problem: given a graph G that has property P, find a minimal spanning subgraph of G with property P. We describe general algorithms for this problem and prove their correctness under fairly weak assumptions about P. We establish that the worst-case running time of these algorithms is $\Theta(m + n \log n)$ for 2-edge-connectivity and biconnectivity where n and m denote the number of vertices and edges, respectively, in the input graph. By refining the basic algorithms we obtain the first linear time algorithms for computing a minimal 2-edge-connected spanning subgraph and for computing a minimal biconnected spanning subgraph. We also devise general algorithms for computing a minimal spanning subgraph in directed graphs. These algorithms allow us to simplify an earlier algorithm of Gibbons, Karp, Ramachandran, Soroker, and Tarjan for computing a minimal strongly connected spanning subgraph. We also provide the first tight analysis of the latter algorithm, showing that its worst-case time complexity is $\Theta(m + n \log n)$.

Let H be a bipartite graph with bipartition (A, B) where IAI = n and every subset X of A with at most a n elements has at least blXl neighbors (a ~1, b > 1).We consider the problem of computing a matching from a given subset X ~A of size at most a n into l?.By Hall's theorem such a matchhg doea indeed exist.We propose two algorithms for this problem.The first algorithm is in NC for b ~d' for a constant e > O; here d denotes the maximum degree of a vertex in A. The second algorithm uses randomization and computes a matching for X provided b = 0(/-).It terminates in O(log n) steps for constant d and in Polylog(n) time for d = C@olylog(n))(with high probability).This algorithm is a local algorithm in the sense that the vertices in the graph establish the matching themselves in an online fashion.Both algorithms have applications to local and global routing in communication networks.In particular our results improve a construction of a self-routing nonblocking network by Arora, Leighton, and Maggs.

A maximal independent set in a hypergraph is a subset of vertices that is maximal with respect to the property of not containing any edge of the hypergraph. We show that an algorithm proposed by Beame and Luby is in randomized NC for hypergraphs in which the maximum edge size is bounded by a constant. To prove this, we bound the upper tail of sums of dependent random variables defined on the edges of a hypergraph. These bounds may be viewed as extensions of bounds on the tail of the binomial distribution. We derandomize this algorithm to obtain the first sublinear time deterministic algorithm for hypergraphs with edges of size O(1). The algorithm exhibits the following time-processor tradeoff: it can be made to run in time O(ne) with nO(1/e) processors for a hypergraph on n vertices, for any e ≥ 2d+1• (log log n)/(log n); here d = O(1) denotes the maximum size of an edge in H. In particular, for any constant e > O, we have an algorithm running in time O(ne) on a polynomial number of processors, and we have an algorithm running in time (log n)O(1) on nO(log n/log log n) processors.