Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Position Paper: Formal Methods in Agile Development
Get PDFModern software development must be agile. It has to accept that soft- ware systems undergo a lot of changes due to changes in the application context (for example changing conditions on the markets and changes due to the jurisdiction) and base technology (e.g. integration of new frameworks or updates of the platform) in their life cycle. Thus, most of the activities in the development process are redesign steps. Even requirements are not stable. They change in time as the context of the system changes. There is no time for complex correctness proofs of the implementation with respect to the requirements. Automatic (regression) testing has proved to be sufficient for correct system behaviour. Therefore the agile developer does not learn and apply formal methods himself. In order to be agile, however, he relies on tools for automatic refactoring of the system or of certain parts of it. These tools are able to change the system structure without changing its behaviour. We argue in this paper that, in order to build such tools, further research in the area of formal system modelling and development is needed
Parallelism and Concurrency Theorems for Rules with Nested Application Conditions
Get PDFWe present Local Church-Rosser, Parallelism, and Concurrency Theorems for rules with nested application conditions in the framework of weak adhesive HLR categories including different kinds of graphs. The proofs of the statements are based on the corresponding statements for rules without application conditions and two Shift-Lemmas, saying that nested application conditions can be shifted over morphisms and rules
A lightweight abstract machine for interaction nets
Get PDFWe present a new abstract machine for interaction nets and demonstrate
that an implementation based on the ideas is significantly more efficient than existing interaction net evaluators. The machine, which is founded on a chemical abstract machine formulation of interaction nets, is a simplification of a previous abstract machine for interaction nets. This machine, together with an implementation, is at the heart of current work on using interaction nets as a new foundation as an intermediate language for compiler technology
Systemic Modeling of Agent Coaction: A Catalog of Decentralized Coordinating Processes
Get PDFTaking inspiration from natural self-organizing systems is a successful
strategy to solve computational problems in distributed systems. Faced with a particular
problem, application designers have to identify an appropriate dynamical behavior
and decide how to induce similar behavioral modes. In order to consolidate
these ad-hoc activities to a systematic dynamical design method, we discuss and exemplify
a behavioral modeling approach that describes the macroscopic behavior of
agent-based software systems. This formalism is used to catalog the dynamic behavior
of prominent examples of natural self-organizing systems. These here presented
models represent generic, reusable templates for decentralized system adaptations
that serve as analysis templates for application designs. A tailored programming
model allows to supplement these templates in agent-based software applications
with minimal intervention in the agent models
The Pattern Instance Notation: A Simple Hierarchical Visual Notation for the Dynamic Visualization and Comprehension of Software Patterns
Get PDFDesign patterns are a common tool for developers and architects to understand and reason about a software system. Visualization techniques for patterns have tended to be either highly theoretical in nature, or based on a structural view of a system’s implementation. The Pattern Instance Notation is a simple visualization technique for design patterns and other abstractions of software engineering suitable for the programmer or designer without a theoretical background. While based on a formal representation of design patterns, using PIN as a tool for comprehension or reasoning requires no formal training or study. PIN is hierarchical in nature, and compactly encapsulates abstractions that may be spread widely across a system in a concise graphical format, while allowing for repeated unveiling of deeper layers of complexity and interaction on demand. It is designed to be used in either a dynamic visualization tool, or as a static representation for documentation and as a teaching aid
Markov Abstractions for Probabilistic Pi-Calculus
Get PDFThis paper presents a range of approaches to the analysis and development of program specifications that have been expressed in a probabilistic process algebra. The approach explores Markovian processes as a high-level abstraction tool to reason about system specifications. The abstractions include ones to check the structure of specifications, analyze the long-term stability of the system, and provide guidance to improve the specifications if they are found to be unstable. The approach could present interest to the formal methods and critical-systems development community, as it leads to an automatic analysis of some subtle properties of complex systems. We illustrate some aspects by analyzing the Monty Hall game, and a probabilistic protocol
MLContext: A Context-Modeling Language for Context-Aware Systems
Get PDFContext awareness refers to systems that can both sense and react based on their environment. The complexity of these systems makes necessary to apply software engineering techniques in their development, such as Model-Driven Software development (MDD). One of the main difficulties that developers of context-aware systems must tackle is how to manage the needed context information. In this paper, we present MLContext, a textual Domain Specific Language (DSL) which is specially tailored for modeling context information and automatically generating software artefacts from context models. It has been designed to provide a high-level abstraction, to be an easy to learn, and to promote reuse of context models. We have built a toolkit including an editor and a parser to convert MLContext textual specifications into models. As a proof of concept, we have automatically generated ontologies and Java code for the OCP middleware. MLContext models can be reused in applications with the same context because they do not include details related to the platforms or the implementation. These context models can be specified by non-developers users because MLContext provides high-level abstractions of the domain
Model-Based Engineering of Supervisory Controllers using CIF
Get PDFIn the Model-Based Engineering (MBE) paradigm, models are the core elements in the design process of a system from its requirements to the actual implementation of the system. By means of Supervisory Control Theory (SCT), supervisory controllers (supervisors) can be synthesized instead of designing them manually. In this paper, a framework based on the Compositional Interchange Format for hybrid systems (CIF) has been developed that integrates the MBE and the SCT paradigms. To illustrate the framework, an industrial-size case study has been performed: 'synthesis of a supervisory controller for the patient
support system of an MRI scanner'. In this case study, we address 1) modelling of the components and the control requirements;
2) synthesis of the supervisor;
3) simulation of the synthesized supervisor and a hybrid model of the plant; and
4) real-time, simulation based control of the supervisor and the actual patient support system of the MRI scanner
Requirements Analysis for an Integrated OCL Development Environment
Get PDFAn Integrated OCL Development Environment (IDE4OCL) can significantly improve the pragmatics and praxis of OCL. We present the domain concepts, toolâlevel interactions with OCL and the use cases we identified in a systematic analysis of requirements for an IDE4OCL. The domain concepts is an important contribution of our work as it attempts to clarify inconsistencies in the relevant specifications. Because OCL is not a standâalone language, the OCL landscape includes several interacting tools including an IDE4OCL. The use cases describe our vision of the desired functionality unique to an IDE4OCL. The results of our analysis and the long term vision of our work should be relevant to developers of OCL tools as well as to the OMG Request for Information regarding the UML Futures1. Our work is relevant to the UML Futures Roadmap because providing OCL for the constraints in the UML specification has been a longstanding problem at the OMG
An Active Pattern Infrastructure for Domain-Specific Languages
Get PDFTool support for design patterns is a critically important
area of computer-aided software engineering. With the proliferation
of Domain-Specific Modeling Languages (DSMLs), the adaptation of the
notion of design patterns appears to be a promising direction of
research. This paper introduces a new approach to DSML patterns,
namely, the Active Model Pattern infrastructure. In this framework,
not only the traditional insertion of predefined partial models is
supported, but interactive, localized design-time manipulation of
models. Optionally, the infrastructure can be adapted to handling
transactional tracing information as well as transactional undo and
redo operations. Possible realizations of the framework are also
discussed and compare