Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
On formalising interactive number entry on infusion pumps
Get PDFWe define the predictability of a user interface as the property that an idealised user can predict with sufficient certainty the effect of any action in a given state in a system, where state information is inferred from the perceptible output of the system. In our definition, the user is not required to have full knowledge of a history of actions from an initial state to the current state. Typically such definitions rely on cognitive and knowledge assumptions; in this paper we explore the notion in the situation where the user is an idealised expert and understands perfectly how the device works. In this situation predictability concerns whether the user can tell what state the device is in and accurately predict the consequences of an action from that state simply by looking at the device; normal human users can certainly do no better. We give a formal definition of predictability in higher order logic and explore how real systems can be verified against the property. We specify two real number entry interfaces in the healthcare domain (drug infusion pumps) as case studies of predictable and unpredictable user interfaces. We analyse the specifications with respect to our formal definition of predictability and thus show how to make unpredictable systems predictable
Reachability Analysis on Timed Graph Transformation Systems
Get PDFIn recent years, software increasingly exhibits self-* properties like selfoptimization
or self-healing. Such properties require reconfiguration at runtime in
order to react to changing environments or detected defects. A reconfiguration might
add or delete components as well as it might change the communication topology of
the system. Considering communication protocols between an arbitrary number of
participants, reconfiguration and state-based protocol behavior are no longer independent
from each other and need to be verified based on a common formalism. Additionally,
such protocols often contain timing constraints to model real-time properties.
These are of integral importance for the safety of the modeled system and thus
need to be considered during the verification of the protocol. In current approaches
either reconfigurations or timing constraints are not considered. Existing approaches
for the verification of timed graph transformation systems lack important constructs
needed for the verification of state-based real-time protocol behaviors. As a first
step towards a solution to this problem, we introduced Timed Story Driven Modeling
[HHH10] as a common formalism integrating state-based real-time protocol
behaviors and system reconfigurations based on graph transformations.
In this paper, we introduce a framework allowing to perform reachability analysis
based on Timed Story Driven Modeling. The framework allows to compute the
reachable timed graph transition system based on an initial graph and a set of timed
transformation and invariant rules
Incremental Pattern Matching in Graph-Based State Space Exploration
Get PDFGraph pattern matching is among the most costly operations in any graph transformation system. Incremental pattern matching aims at reducing this cost by incrementally updating, as opposed to totally recalculating, the possible matches of rules in the graph grammar at each step of the transformation. In this paper an implementation of one such algorithm is discussed with respect to the GROOVE
toolset, with a special emphasis put on state space exploration. Specifically, we shall discuss exploration strategies that could better harness the positive aspects of
incremental pattern matching in order to gain better performance
Preface
Get PDFCollocated with the ACM/IEEE International Conference on Model-Driven Engineering Languages and Systems (MODELS), the Educators’ Symposium (EduSymp) focuses on the huge topic of software modeling education ranging from experience reports and case studies to novel pedagogical approaches. In the following, we shortly report on the 6th EduSymp held in October 2010 in Oslo
Aligning OCL with UML
Get PDFOCL is widely used by UML and other languages to constrain meta-models and perform evaluations on models.
Unfortunately no OCL 2.x specification has ever been aligned with any UML 2.x specification. This lack of alignment makes some OCL compliance points such as XMI interchange unachievable. This paper describes how introduction of an OCL Pivot Meta-Model and clear exposition of the Values package may provide a solution to the alignment and a variety of other specification issues
OCL-based Runtime Monitoring of JVM hosted Applications
Get PDFIn this paper we present an approach that enables users to monitor and verify the behavior of an application running on a virtual machine at the model level. Concrete implementations of object-oriented software usually contain a lot of technical
classes. Thus, the central parts of an application, e.g., the business rules, may be hidden among peripheral functionality like user-interface classes or classes managing persistency. Our approach makes use of modern virtual machines and allows the devloper to profile an application in order to achieve an abstract monitoring and verification of central application components. We represent virtual machine
bytecode in form of a so-called platform-aligned model (PAM) comprising OCL invariants and pre- and postconditions. In contrast to related work, our approach uses the original source or bytecode of the monitored application as it stands and does not require any changes. We show a prototype implementation as an extension of the UML and OCL tool USE. Also, we investigate the impact of our approach to the execution time of a monitored system
Closure and Attention Activation in Human Automatic Behaviour: A Framework for the Formal Analysis of Interactive Systems
Get PDFAutomatic behaviour can be defined as a fast processing
human activity that does not require attention to occur.
According to Norman and Shallice's model of attention and
automaticity the majority of responses are under fairly automatic
control triggered by environmental cues.
In this paper we define a process algebraic framework to
formalise Norman and Shallice's model and illustrate it through
two case studies: Driving and using an Automatic Teller
Machine (ATM).
Finally we show how to use model-checking to analyse model
instantiations and present the outcome of the analysis for the
ATM case study
A Process Algebraic Description of a Temporal Wireless Network Protocol
Get PDFThe problem of coordination is central to research in robotics, automatically guided vehicles, autonomous cars, unmanned aerial vehicles, and any other areas in which autonomous agents of any kind operate concurrently. This paper focuses on one particular model of coordination, namely Comhord´u. The contribution of this work is a formalisation of the existing model in precise mathematical terms. This formalisation extends our understanding of the model and provides a basis for future work such as the formal verification of model properties, e.g. system safety
Active Model Patterns with Interactive Model Transformation
Get PDFWith the proliferation of domain-specific languages, the generalization of OO patterns is a natural demand. Concepts and tools supporting pattern specification and execution for arbitrary domain-specific languages facilitate to meet these
requirements. Our previous work introduced the Active Model Pattern Infrastructure and possible realizations for its static aspect. In this paper, we contribute a realization for the operational aspect of the framework. We propose graph rewriting-based interactive model transformation to describe and automate often recurring operational patterns in domain-specific modeling. We have extended a general transformation
system with localized application of the rules and facilitate run-time customization possibilities for the domain engineer to influence the execution of the operations. We can specialize this approach to provide an implementation of the static aspect as well. We have realized our solution in the Visual Modeling and Transformation System
