Search

Despite significant advances in the development of model checking, it remains a difficult task in the hands of experts to make it scale to the size of industrial systems. A key step in achieving scalability is to "divide-and-conquer", that is, to break up the veri.cation of a system into smaller tasks that involve the verification of its components. Assume-guarantee reasoning [9, 11] is a widespread "divide-and-conquer" approach that uses assumptions when checking individual components of a system. Assumptions essentially encode expectations that each component has from the rest the system in order to operate correctly. Coming up with the right assumptions is typically a non-trivial manual process, which limits the applicability of this type of reasoning in practice. [ABSTRACT FROM AUTHOR]

The regulation of multiagent systems may be approached from different stand-points. In this paper I will take the perspective of using a certain type of devices, electronic institutions, to regulate agent interactions. Furthermore, in this paper I am concerned with the tasks of design and construction of actual electronic institutions and I will explore some of the empirical aspects that one may encounter in such activities. More specifically, I will focus on those empirical aspects that are characteristic of electronic institutions rather than those that may be typical of multi-agent systems development in general or other types of software engineering. I use three examples of actual electronic institutions that show different and complementary features in order to motivate a number of distinctions that may be used to treat empirical features in a systematic way. [ABSTRACT FROM AUTHOR]

The CSDUML 2006 workshop is a continuation of the series regarding development of critical systems using modeling languages. The report summarizes papers presented and discussion at the workshop. [ABSTRACT FROM AUTHOR]

Changes and adaptations are always necessary after the deployment of a multiagent system (MAS), as well as of any other type of software systems. Some of these changes may be simply perfective and have local impact only. However, adaptive changes to meet changed situations in the operational environment of the MAS may have global impact on the overall design. In this paper, we analyze the issue of continuous design change/adaptation in a MAS organization, and the specific problem of how to properly model/design a MAS so as to make it ready to adaptation. Following, the paper focuses on the Gaia methodology and analyzes - also with the help of an illustrative example - its suitability in supporting and facilitating adaptive changes in MASs organizations, and its advantages and limitations with this regard over a number of different agent-oriented methodologies. Keywords: Agent Oriented Methodologies, Design for Change, Adaptive Organizations, Methodologies Evaluation. [ABSTRACT FROM AUTHOR]

We describe a test development method, named OTK, that is aimed at optimizing compiler testing. The OTK method is based on constructing a model of optimizer's input data. The method allows developing tests targeted to testing a chosen optimizer. A formal data model is constructed on the basis of an abstract informal description of an algorithm of the optimizer under test. In the paper, we consider in detail the process of analyzing an optimization algorithm and building a formal model. We also consider in outline the other part of the method, test selection and test running. The OTK method has been successfully applied in several case studies, including test development for several different optimizing compilers for modern architectures. [ABSTRACT FROM AUTHOR]

The first edition of the workshop Models@run.time was co-located with the ACM/IEEE 9th International Conference on Model Driven Engineering Languages and Systems (formerly the UML series of conferences). The workshop took place in the antique city of Genoa, Italy, on the 1st of October, 2006. The workshop was organised by Gordon Blair, Robert France, and Nelly Bencomo. This summary gives an overview an account of the presentations and lively discussions that took place during the workshop. [ABSTRACT FROM AUTHOR]

The workshop OCLApps 2006 was organized as a part of MoDELS/UML Conference in Genova, Italy. It continues the series of five OCL (Object Constraint Language) workshops held at previous UML/MoDELS conferences between 2000 - 2005. Similar to its predecessors, the workshop addressed both people from academia and industry. The advent of the MDA (Model Driven Architecture) vision and the rapid acceptance of MDE (Model Driven Engineering) approaches emphasize new application domains (like Semantic Web or Domain Specific Languages) and call for new OCL functionalities. In this context, the OCLApps 2006 Workshop, was conceived as a forum enabling researchers and industry experts to present and debate how the OCL could support these new requirements. [ABSTRACT FROM AUTHOR]

Engineering component interactions is a major challenge in the development of large-scale, open systems. In the realm of multiagent system research, organizational abstractions have been proposed to overcome the complexity of this task. However, the gap between these modeling abstractions, and the constructs provided by todays agent-oriented software frameworks is still rather big. This paper reports on the multiagent programming framework, which provides executable constructs for each of the organizational, ACL-based modeling abstractions of the theory. Setting out from a components and connectors perspective on the elements of the metamodel, their executions semantics is defined and instrumented on top of the JADE platform. Moreover, a systematic reuse approach to the engineering of interactions is put forward. [ABSTRACT FROM AUTHOR]

Formal methods constitute a means of developing reliable and correctly behaving software based on a specification. In scenarios where information technology is used as a foundation to enable human communication, this is, however, not always enough. Successful interaction between humans often depends on the concept of trust, which is different from program correctness. In this paper, we present a framework for integrating trust into a formal development process, allowing for the construction of formally correct programs for communication, embracing trust as a central concept. We present a coordination language for use with action systems, taking a modular approach of separating trust aspects from other functionality. We also believe that our work can be adapted to modelling other aspects beside trust. Throughout the paper, we employ a case study as a testbed for our concepts. [ABSTRACT FROM AUTHOR]

By a domain we mean a universe of discourse. Typical examples are (partially) man-made universes of discourse - such as Air Traffic, Airports, Financial Services (banks, insurance companies, securities trading [brokers, traders, stock exchanges]), Health Care (hospitals etc.), Secure IT Systems (according to Intl. ISO/IEC Standard 17799), The Market (consumers, retailers, wholesalers, producers, "the supply chain"), Transportation (road, air, sea and/or rail transport), etc. We shall outline how one might describe such (infrastructure component) domains, informally and formally - what the current descriptional limitations appear to be, and, hence, the prospects for future research as well as practice. The current paper is based on Part IV, Chaps. 8-16 of [3]. The volume is one of [1,2,3]. The aim of this paper is to suggest a number of areas of domain theory and methodology research. [ABSTRACT FROM AUTHOR]

The TCP/IP/Ethernet protocol is considered not suitable for use in real-time control systems. It deals with a lack of time determinism, which characterizes fieldbuses. Nevertheless several corporations propose networking based on the TCP/IP/Ethernet even for control purposes with some modifications of the standard however. This paper examines possibility of application of the TCP/IP/Ethernet communication without modifications (introducing also Internet as one of tested cases) for feedback control purposes. Experimental investigations have been performed in four stages. In the beginning tests of network properties, including tests of transmission time and packet loss measurements have been performed. Three following stages show experimental testing of feedback control, when TCP/IP transmission occurs between PI controller and control plant. Three representative platforms have been chosen for testing: LabVIEW, RSLogix and Simatic. The main and original contribution presented in this paper is design and construction of three test stands as well as methodology of testing experiments. Standard control over analog channel has been also presented as comparison. The results of testing show acceptable performance of control via TCP/IP/Ethernet networking. [ABSTRACT FROM AUTHOR]

In this paper we extend $\mathcal{HOTL}$ (Hypotheses and Observations Testing Logic) to provide a formal framework to test timed systems. The main idea underlying $\mathcal{HOTL}$ is to infer whether a set of observations (i.e., results of test applications) allows to claim that the IUT conforms to the specification if a specific set of hypotheses is assumed. In this paper we adapt $\mathcal{HOTL}$ to cope with the inclusion of time issues. In addition, we show the soundness and completeness of the new framework, that we call $\mathcal{THOTL}$, with respect to a general notion of timed conformance. [ABSTRACT FROM AUTHOR]

Reasoning about functional programs is simpler than reasoning about their imperative counterparts. However, finding bugs in lazy functional languages has been more complex until quite recently. The reason was that not much work was done on developing practical debuggers. Fortunately, several debuggers exist nowadays. One of the easiest to use Haskell debuggers is Hood, whose behavior is based on the concept of observation of intermediate data structures. However, although using Hood can be simple when observing some structures, it is known that it can be hard to understand how it works when dealing with complex situations. In this paper, we formalize the behavior of the Hood debugger by extending Sestoft's natural semantics. Moreover, we also indicate how to derive an abstract machine including such debugging information. By doing so, we do not only provide a formal foundation, but we also provide an alternative method to implement debuggers. In fact, we have already implemented a prototype of the abstract machine commented in this paper. [ABSTRACT FROM AUTHOR]

A persistent computing system is a reactive system that functions continuously anytime without stopping its reactions even when it needs to be maintained, upgraded, or reconfigured, it has some trouble, or it is attacked. However, the requirement that a computing system should run continuously and persistently is never taken into account as an essential and/or general requirement by traditional system design and development methodologies. As a result, there is no clearly defined standard to be used for measuring the reactability of a computing system. This paper proposes the first method to measure the reactability of a persistent computing system in a unified way. The paper introduces the notion of reactive processing path among components and shows that the reactive processing paths can be used to measure the reactability of a persistent computing system. [ABSTRACT FROM AUTHOR]

This paper describes a process-algebraic approach to specification and refinement of workflow processes. In particular, we model both specification and implementation of workflows as CSP processes. CSP's behavioural models and their respective refinement relations not only enable us to prove correctness properties of an individual workflow process against its behavioural specification but also allows us to design and develop workflow processes compositionally. Moreover, coupled with CSP is an industrial strength automated model checker FDR, which allows behavioural properties of workflow models to be proved automatically. This paper details some CSP models of van der Aalst et al.'s control flow workflow patterns, and illustrates behavioural specification and refinement of workflow systems with a business process scenario. [ABSTRACT FROM AUTHOR]

In this paper, we report on the development of a methodology for the evolution of software towards new architectures. In our approach, we represent source code as graphs. This enables the use of graph transformation rules, allowing the automation of the transformation process. Prior to its model representation, the source code is subject to a preparatory step of semi-automatic code annotation according to the contribution of each of its parts in the target architecture. This paper first describes the overall methodology and then focuses on the code annotation and model transformation parts. We also discuss issues of the implementation of the approach based on existing tools. [ABSTRACT FROM AUTHOR]

A key issue with Web Services (WS) is the verification and validation (V&V) of services to build trust between service providers and service users. This paper proposed a test-broker architecture so that all stakeholder within WS can contribute to improve the testing of the services. The test broker supports the submission, indexing, and querying of test artifacts such as test cases, defect reports and evaluations. It can also provide the services for the test generation, test coordination, and distributed testing services. The DCV&V (Decentralized, Collaborative, Verification and Validation) framework is proposed with a set of distributed and collaborated test brokers dedicated to different V&V tasks to enable scalable and flexible test collaborations. The paper explores the concept of design-by-contract and applies the principle to DCV&V. It identifies two categories of testing contracts including TSC (Testing Service Contracts) and TCC (Test Collaboration Contracts). It illustrates the application of TSC with contract-based test generation based on WS OWL-S specification. It elaborates TCC with the analysis of the test artifacts definitions. [ABSTRACT FROM AUTHOR]

Fujaba is an UML [21] based CASE tool with an emphasis on code generation from graphical behavior specifications. The Fujaba tool is accompanied by the Fujaba process, a systematic approach to use Fujaba for system development [5]. To improve the tool support for the Fujaba process, we have developed the XProM plug-in. This paper exemplifies how the XProM plug-in supports the tool developer in following the Fujaba Process. Main parts of this paper are a tutorial to XProM users. However, the paper is also useful for other CASE tool developers as a guide how developers could be supported. Therefore, we also give some hints, how such a support may be realized. As a running example we use the development of model transformations for a simple statechart editor. [ABSTRACT FROM AUTHOR]

In the medical domain, there is a tendency to standardize health care by providing medical guidelines as summary of the best evidence concerning a particular topic. Based on the assumption that guidelines are similar to software, we try to carry over techniques from software engineering to guideline development. In this paper, we show how to apply formal methods, namely interactive verification to improve the quality of guidelines. As an example, we have worked on a guideline from the American Academy of Pediatrics for the management of jaundice in newborns. Contributions of this paper are as follows: (I) a formalized model of a nontrivial example guideline, (II) an approach to verify properties of medical guidelines interactively, and (III) verification of a first example property.This work has been partially funded by the European Commission's IST program, under contract number IST-FP6-508794 Protocure II. [ABSTRACT FROM AUTHOR]

This paper ascribes a formal semantics to advice weaving in AspectJ. Since the version 1.1, AspectJ language is developed using bytecode weaving, which combines aspects and classes to produce ".class" files that run in a Java Virtual Machine (JVM). In AspectJ, advice weaving is done statically by inserting the advice functionality in some regions of the code. These regions are join points that are declared using pointcuts. In this paper, we focus only on static pointcuts, i.e., pointcuts that correspond directly to locations in the bytecode. AspectJ dynamic pointcuts such as target, this, and cflow are not in the focus of this paper. [ABSTRACT FROM AUTHOR]

Over the past twenty-five years or so Saddleback search has been used as an paradigm of how methods of formal program construction can quickly lead to a simple and effective algorithm for searching an ordered table. In this paper we revisit the problem and show that saddleback search is not in fact the best algorithm when one dimension of the table is much smaller than the other. The paper is structured in the form of a classroom discussion involving a teacher and four very clever students. [ABSTRACT FROM AUTHOR]

This paper has an introductory nature. It sets the scene for the three papers in the thematic session "Structured Data Tools". We discuss interaction and coordination in general and look more specifically at the XML data format and the dataflow driven coordination language Reo. [ABSTRACT FROM AUTHOR]

This paper describes how to refine a Gaia design by applying agent-oriented extensions of UML. First, we show how the Gaia Interaction model can be improved by applying the first two layers of the Agent Interaction Protocol (AIP) of AUML. Second, Gaia Agent and Service models are refined by applying the AIP's third layer combined with Extended UML Class Diagrams. Third, Gaia Organisational Structure is enriched by applying the Aalaadin model. The final aim of the whole process is to obtain a more concrete design closer to implementation. We demonstrate how the refinement process can be applied to the development of an agent-based system for conference management. [ABSTRACT FROM AUTHOR]

The Model Driven Architecture (MDA) involves automated trans-formations between software models defined in different languages at different abstraction levels. This paper takes an MDA approach to integrate a formal modeling language (Object-Z) with an informal modeling language (UML) via model transformation. This paper shows how formal and informal modeling languages can be cooperatively used in the MDA framework and how the trans-formations between models in these languages can be achieved using an MDA development environment. The MDA model transformation techniques allow us to have a reusable transformation between formal and informal modeling languages. The integrated approach provides an effective V&V technique for the MDA. [ABSTRACT FROM AUTHOR]

The present movement in the adoption of agile methodologies as a contemporary approach to the management of the software development processes has seen a growing trend towards the selection of relevant practices from the agile family as opposed to the adoption of specific methods. This paper reports work-in-progress of a proposed novel modeling technique for tailoring methodologies to a particular environment using the family of methodologies approach. The tool is being applied by one software development organisation in Southern Africa and the partial results are included in this paper. [ABSTRACT FROM AUTHOR]

Source repositories are a promising database of information about software projects. This paper proposes a tool to extract and summarize information from CVS logs in order to identify whether there are differences in the development approach of Agile and non-Agile teams. The tool aims to improve empirical investigation of the Agile Methods (AMs) without affecting the way developers write code. There are many claims about the benefits of AMs; however, these claims are seldom supported by empirical analysis. Configuration management systems contain a huge amount of quantitative data about a project. The retrieval and part of the analysis can be automated in order to get useful insights about the status and the evolution of the project. However, this task poses formidable challenges because the data source is not designed as a measurement tool. This paper proposes a tool for extracting and summarizing information from CVS (Concurrent Versions System) repositories and a set of analysis that can be useful to identify common or different behaviors. [ABSTRACT FROM AUTHOR]

This paper shows how System Metaphor delivers a coherent system of names that carry more information than unrelated names would. Keywords: Extreme Programming, Metaphor, Names. [ABSTRACT FROM AUTHOR]

Extreme programming (XP) has been introduced in various scenarios primarily because some in industry argued for a move away from what they feel are rigid documentation-based development techniques. This has usually taken place with experienced developers. This paper describes attempts by researchers from the University of Sheffield to introduce XP to relatively inexperienced student developers. This paper describes some of the important findings and provides evidence relating to common problems encountered when students attempt to adjust to XP. Keywords: Extreme Programming, Agile Methods, Empirical Software Engineering [ABSTRACT FROM AUTHOR]

Early Aspects are aspects found in the early life cycle phases of software development, including requirements elicitation and analysis, domain analysis and architecture design activities. Aspects at these stages crosscut the modular units appropriate for their lifecycle activity; traditional requirements documentation, domain knowledge capture and architectural artifacts do not afford separate description of early aspects. As such, early aspects necessitate new modularizations to be effectively captured and maintained. Without new tools and techniques, early aspects remain tangled and scattered in lifecycle artifacts, and may lead to development, maintenance and evolution difficulties. [ABSTRACT FROM AUTHOR]

Constraint Programming (CP) technology has been extensively used in Random Functional Test Generation during the recent years. However, while the existing CP methodologies are well tuned for traditional combinatorial applications e.g. logistics or scheduling, the problem domain of functional test generation remains largely unexplored by the CP community and many of its domain specific features and challenges are still unaddressed. In this paper we focus on the distinctive features of CP for the random functional test generation domain and show how these features can be addressed using a classical CP engine with custom extensions. We present some modeling and solving problems arising in this context and propose solutions. In particular, we address the way of model building in the problem domain of test generation which we refer to as multi-layer modeling. In this context we introduce constraint patterns of composite variable, implied condition and implied composite variable condition, define their semantics and propose schemes for their CSP modeling. The paper also addresses specific problems arising at the solving stage in the problem domain of random test generation. We propose solutions to these problems by means of custom random search algorithms. This approach is illustrated on the examples of the disjunction constraint and conditional variable instantiation. The latter algorithm addresses the feature of dynamic modeling required in the test generation task. To demonstrate the effectiveness of our approach we present experimental results based on the implementation using ILOG Solver as a CP engine. [ABSTRACT FROM AUTHOR]

In this paper we introduce a Prover-Verifier model for analyzing the computational complexity of a class of Constraint Satisfaction problems termed Binary Boolean Constraint Satisfaction problems (BBCSPs). BBCSPs represent an extremely general class of constraint satisfaction problems and find applications in a wide variety of domains including constraint programming, puzzle solving and program testing. We establish that each instance of a BBCSP admits a coin-flipping Turing Machine that halts in time polynomial in the size of the input. The prover P in the Prover-Verifier model is endowed with very limited powers; in particular, it has no memory and it can only pose restricted queries to the verifier. The verifier on the other hand is both omniscient in that it is cognizant of all the problem details and insincere in that it does not have to decide a priori on the intended proof. However, the verifier must stay consistent in its responses. Inasmuch as our provers will be memoryless and our verifiers will be asked for extremely simple certificates, our work establishes the existence of a simple, randomized algorithm for BBCSPs. Our model itself serves as a basis for the design of zero-knowledge machine learning algorithms in that the prover ends up learning the proof desired by the verifier. [ABSTRACT FROM AUTHOR]

Test effectiveness is a central quality aspect of a test specification which reflects its ability to demonstrate system quality levels and to discover system faults. A well-known approach for its estimatation is to determine coverage metrics for the system code or system model. However, often these are not available as such but the system interface only, which basically define structural aspects of the stimuli and responses to the system. Therefore, this paper focuses on the idea of using test data variance analysis as another analytical approach to determine test quality. It presents a method for the quantitative evaluation of structural and semantical variance of test data. Test variance is defined as the test data distribution over the system interface data domain. It is expected that the more the test data varies, the better the system is tested by a given test suite. The paper instantiates this method for black-box test specifications written in TTCN-3 and the structural analysis of send templates. Distance metrics and similarity relations are used to determine the data variance. [ABSTRACT FROM AUTHOR]

This paper uses Participatory Semantics to explicate commitment. Information expresses the fact that a system is in a certain configuration that is correlated to the configuration of another system. Any physical system may contain information about another physical system. For the purposes of this paper, physical commitment is defined to be information pledgedabout physical systems (situated at a particular place and time). This use of the term physical commitment is currently nonstandard. Note that commitment is defined for whole physical system; not just a participant or process. Organizational and social commitments can be analyzed in terms of physical commitments. For example systems that behave as scientific communities can have commitments for monotonicity, concurrency, commutativity, pluralism, skepticism, and provenance. Speech Act Theory has attempted to formalize the semantics of some kinds of expressions for commitments. Participatory Semantics for commitment can overcome some of the lack of expressiveness and generality in Speech Act Theory. [ABSTRACT FROM AUTHOR]

Hierarchical structures have been widely used by human organizations because they provide the natural means to delegate tasks, to reduce communication lines and to control the activities performed into them. This has motivated the development of different approaches to automate many of the activities that take place in hierarchical organizations. Recent frameworks, such as Gaia, Aalaadin, HarmonIA and OperA, among others, have considered the agent paradigm to do so without taking into account that organizations are dynamic entities that evolve with the time and, consequently, agents must adapt to changes. Here we develop a model for flexible and open hierarchical organizations where agents can dynamically adapt themselves to organizational changes. [ABSTRACT FROM AUTHOR]

The viability of the application of the e-Institution paradigm for obtaining overall desired behavior in open multiagent systems (MAS) lies in the possibility of bringing the norms of the institution to have an actual impact on the MAS. Institutional norms have to be implemented in the society. The paper addresses two possible views on implementing norms, the so-called regimentation of norms, and the enforcement of norms, with particular attention to this last one. Aim of the paper is to provide a theory for the understanding of the notion of enforcement and for the design of enforcement mechanisms in e-Institutions. [ABSTRACT FROM AUTHOR]

Support for new forms of organization and social interaction requires understanding the influence of structure on behavior. Goal dependencies indicate some relationship between roles, through which actions can be coordinated. Social relationships determine different types of power links between roles. Efficient coordination requires that goal dependency and power structure are well tuned to each other. In this paper, we will investigate what is the exact nature of this relationship between roles in an organization and what are the consequences of different structure forms. We will also see what is the difference if the relations are not hierarchical but organized through a market or network structure. [ABSTRACT FROM AUTHOR]

Artificial Intelligence has contributed (formal) design models and software support tools to application areas such as architecture, engineering and software design This paper explores the effectiveness of applying design models to the area of organization (re)design. To that purpose a component-based model for (re)design of organizations is presented as a specialization of an existing generic design model. Using recently developed formalizations within Organization Theory organization models are described as design object descriptions, and organization goals as design requirements. A design process specification is presented that models the redesign process for an organization that adapts to changes in the environment. The formally specified and implemented approach to organization redesign thus obtained has been tested for a well-known historical case study from the Organization Theory literature. [ABSTRACT FROM AUTHOR]

The language L is used for specifying finite automata, and is a fragment of a first order language with monadic predicates. Checking specification for satisfiability plays an important role in the development of reactive algorithms. Restricted syntax of this language and interpreting it over the integers make it possible to substantially improve resolution-based methods for satisfiability checking. This has been done in previous papers devoted to R- and S-resolution. In this paper, we present yet another improvement based on the restriction of the type of atoms upon which the resolution is allowed. [ABSTRACT FROM AUTHOR]

Graph transformations are one of the best known approaches for defining transformations in model-based software development. They are defined over the abstract syntax of source and target languages, described by metamodels. Since graph transformations are defined on the abstract syntax level, they can be hard to read and require an in-depth knowledge of the source and target metamodels. In this paper we investigate how graph transformations can be made much more compact and easier to read by using the concrete syntax of the source and target languages. We illustrate our approach by defining model refactorings. [ABSTRACT FROM AUTHOR]

This paper develops a model for precisely defining how an agent interacts with objects in its environment through the use of its capabilities. Capabilities are recursively defined in terms of lower-level capabilities and actions, which represent atomic interactions with the environment. Actions are used to represent both sensors and effectors. The paper shows how the model can be used to represent both software and physical agents and their capabilities. The paper also shows how the model can be integrated into the Organization-based Multiagent Systems Engineering methodology. [ABSTRACT FROM AUTHOR]

Remote internet voting incorporates many of the core challenges of trusted global computing. In this paper, we present the Kiezen op Afstand (KOA) system. KOA is a Free Software, remote voting system developed for the Dutch government in 2003/2004. In addition to being Open Source, it is also partially formally specified and verified. This paper summarises the work carried out to date on the KOA system. It charts the evolution of the system, from its initial conception by the Dutch Government, through to its current status. It also describes a roadmap of milestones towards completing its next release: a Free Software, general-purpose, formally specified and verified internet voting system, that incorporates Proof Carrying Code technology for software update and allows trustworthy voting from a mobile phone. We propose that the KOA system should be used as an experimental platform for research in electronic and internet voting; we are not saying that we have solved any of the major problems inherent in voting with computers. [ABSTRACT FROM AUTHOR]

In the context of Service Oriented Computing, contracts are descriptions of the externally observable behaviour of services. Given a group of collaborating services, their contracts can be used to verify whether their composition is sound, i.e., the services are compliant. In this paper, we relate the theory of contracts with the notion of choreography conformance, used to check whether an aggregation of services correctly behaves according to a high level specification of their possible conversations. The main result of this paper is the definition of an effective procedure that can be used to verify whether a service with a given contract can correctly play a specific role within a choreography. This procedure is achieved via composition of choreography projection and contract refinement. [ABSTRACT FROM AUTHOR]

Within model-driven software development, model transformation has become a key activity. It refers to a variety of operations modifying a model for various purposes such as analysis, optimization, and code generation. Most of these transformations need to be bidirectional to e.g. report analysis results, or keep coherence between models. In several application-oriented papers it has been shown that triple graph grammars are a promising approach to bidirectional model transformations. But up to now, there is no formal result showing under which condition corresponding forward and backward transformations are inverse to each other in the sense of information preservation. This problem is solved in this paper based on general results for the theory of algebraic graph transformations. The results are illustrated by a transformation of class models to relational data base models which has become a quasi-standard example for model transformation. [ABSTRACT FROM AUTHOR]

Desharnais, Gupta, Jagadeesan and Panangaden introduced a family of behavioural pseudometrics for probabilistic transition systems. These pseudometrics are a quantitative analogue of probabilistic bisimilarity. Distance zero captures probabilistic bisimilarity. Each pseudometric has a discount factor, a real number in the interval (0, 1]. The smaller the discount factor, the more the future is discounted. If the discount factor is one, then the future is not discounted at all. Desharnais et al. showed that the behavioural distances can be calculated up to any desired degree of accuracy if the discount factor is smaller than one. In this paper, we show that the distances can also be approximated if the future is not discounted. A key ingredient of our algorithm is Tarski's decision procedure for the first order theory over real closed fields. By exploiting the Kantorovich-Rubinstein duality theorem we can restrict to the existential fragment for which more efficient decision procedures exist. [ABSTRACT FROM AUTHOR]

In a seminal paper from 1985, Sistla and Clarke showed that satisfiability for Linear Temporal Logic (LTL) is either NP-complete or PSPACE-complete, depending on the set of temporal operators used . If, in contrast, the set of propositional operators is restricted, the complexity may decrease. This paper undertakes a systematic study of satisfiability for LTL formulae over restricted sets of propositional and temporal operators. Since every propositional operator corresponds to a Boolean function, there exist infinitely many propositional operators. In order to systematically cover all possible sets of them, we use Post's lattice. With its help, we determine the computational complexity of LTL satisfiability for all combinations of temporal operators and all but two classes of propositional functions. Each of these infinitely many problems is shown to be either PSPACE-complete, NP-complete, or in P. Keywords: computational complexity, linear temporal logic. [ABSTRACT FROM AUTHOR]

This paper contributes a technique that expands the set of object invariants that one can reason about in modular verification. The technique uses history invariants, two-state invariants that describe the evolution of data values. The technique enables a flexible new way to specify and verify variations of the observer pattern, including iterators. The paper details history invariants and the new kind of object invariants, and proves a soundness theorem. [ABSTRACT FROM AUTHOR]

Modeling is a hallmark of the practice of engineering. Through centuries, engineers have used models ranging from informal "back of the envelope" scribbles to formal, verifiable mathematical models. Whether circuit models in electrical engineering, heat-transfer models in mechanical engineering, or queuing theory models in industrial engineering, modeling makes it possible to perform rigorous analysis that is the cornerstone of modern engineering. By considering software development as fundamentally an engineering endeavor, RIT's software engineering program strives to instill a culture of engineering practice by exposing our students to both formal and informal modeling of software systems throughout the entire curriculum. This paper describes how we have placed modeling in most aspects of our curriculum. The paper also details the specific pedagogy that we use in several courses to teach our students how to create, analyze and implement models of software systems. [ABSTRACT FROM AUTHOR]

This paper reports on the findings of the first Workshop on Multi-Paradigm Modeling: Concepts and Tools. It contains an overview of the presented papers and of the results of three working groups which addressed multiple views, abstraction, and evolution. Besides this, a definition of the problem space, the main concepts, and an appropriate terminology for multi-paradigm modeling as presented and discussed during the workshop are provided. [ABSTRACT FROM AUTHOR]

Manual administration of complex distributed applications is almost impossible to achieve. On the one side, work in autonomic computing focuses on systems that maintain themselves, driven by high-level policies. Such a self-administration relies on the concept of a control loop. The autonomic computing control loop involves an abstract representation of the system to analyze the situation and to adapt it properly. On the other side, models are currently used to ease design of complex distributed systems. Nevertheless, at runtime, models remain useless, because they are decoupled from the running system, which dynamically evolves. Our proposal, named Dacar, introduces models in the control loop. Using adequate models, it is possible to design and execute both the distributed systems and their autonomic policies. The metamodel suggested in this paper mixes both OMG Deployment and Configuration (OMG D&C) specification and the Event-Condition-Action (ECA) metamodels. This paper addresses the different concerns involved in the control loop and focuses on the metamodel concepts that are required to express entities of the control loop. This paper also gives an overview of our Dacar prototype and illustrates it on a ubiquitous application case study. [ABSTRACT FROM AUTHOR]

This paper reports the application of language metamodeling techniques to EJB3QL, the object-oriented query language for Java Persistence recently standardized in JSR-220. Five years from now, today's EJB3 applications will be legacy. We see our metamodel as an enabler for increasing the efficiency of reverse engineering activities. It has already proven useful in uncovering spots where the EJB3QL spec is vague. The case study reported in this paper involved (a) expressing the abstract syntax and well-formedness rules of EJB3QL in UML and OCL respectively; (b) deriving from that metamodel software artifacts required for several language-processing tasks, targeting two modeling platforms (Eclipse EMF and Octopus); and (c) comparing the generated artifacts with their counterparts in the reference implementation of EJB3 (which was not developed following a language-metamodeling approach). The metamodel of EJB3QL constitutes the basis for applying model-checkers to aid in assuring conformance of tools claiming to support the specification. [ABSTRACT FROM AUTHOR]