Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Approximating Idealised Real-Time Specifications Using Time Bands
Get PDFTimed specifications are often formalised at an absolute level of precision, which does not reflect the real world that the specifications model, i.e., in the real world, inputs cannot be sampled with absolute precision and physical hardware cannot react instantaneously. As a result the developed specifications can often become unimplementable. In this paper, we consider the time bands model which allows time to be structured into several layers of abstraction and relationships between bands to be formalised. This allows the timed specifications developed under idealised assumptions to be approximated using the time band in which the variables are sampled. We implement the approximated specifications using teleo-reactive programs embedded with time bands
An Architecture Description Language for Embedded Hardware Platforms
Get PDFEmbedded software development relies on various tools - compilers, simulators, execution time estimators - that encapsulate a more-or-less detailed knowledge of the target hardware platform. These tools can be costly to develop and maintain:significant benefits could be expected if they were automatically generated from models expressed in a dedicated modeling language.In contrast with Hardware Description Languages (HDLs), that focus on the internal structure and behavior of an electronic board of chip, Hardware Architecture Description Languages consider hardware as a platform for software execution. Such a platform will be described in terms of low-level programming interface (processor instruction set),resources (processing elements, memory and peripheral devices) and elementary services (arithmetic and logic operations, bus transactions).This paper gives an overview of HARMLESS (Hardware ARchitecture Modeling Language for Embedded Software Simulation), a new domain-specific language for modeling embedded hardware platforms. HARMLESS and its associated tools follow the Model-Driven Engineering philosophy: metamodeling and model transformations have been successfully applied to the automatic generation of processor simulators
A Simple Model of Communication APIs – Application to Dynamic Partial-order Reduction
Get PDFWe are interested in the verification, using model checking, of distributed programs that communicate asynchronously over standard communication
APIs such as MPI. This is feasible only if the set of executions that the model checker explores is aggressively reduced to a subset of representative executions, using techniques such as dynamic partial-order reduction. We propose a small set of core primitives in terms of which such APIs can be defined and formally specify these primitives in TLA+.
From this specification we derive theorems about the (in)dependence of invocations of the primitives, and use them in a DPOR-based verifier that runs within SimGrid, a simulation framework for distributed programming.
Our preliminary experimental results indicate that we obtain good reductions, even though complex network operations are implemented in terms of the core commu nication primitives
Towards Test Coverage Criteria for Visual Contracts
Get PDFWhen testing component-based or service-oriented applications we cannot always rely on coverage criteria based on source code. Instead, we have to express our requirements for testing at the interface level. Specifying interfaces by graph transformation rules, so-called visual contracts, we define model-based coverage criteria exploiting the well-known relations of causal dependency and conflict on transformation rules.To this end we establish an observational semantics for graph transformation systems with rule signatures formalising a notion of test execution, and define dependency graphs to provide a structure on which coverage can be analysed
Formal Relationship between Petri Net and Graph Transformation Systems based on Functors between M-adhesive Categories
Get PDFVarious kinds of graph transformations and Petri net transformation systems
are examples of M-adhesive transformation systems based on M-adhesive
categories, generalizing weak adhesive HLR categories. For typed attributed graph
transformation systems, the tool environment AGG allows the modeling, the simulation
and the analysis of graph transformations. A corresponding tool for Petri net
transformation systems, the RON-Environment, has recently been developed which
implements and simulates Petri net transformations based on corresponding graph
transformations using AGG. Up to now, the correspondence between Petri net and
graph transformations is handled on an informal level. The purpose of this paper is
to establish a formal relationship between the corresponding M-adhesive transformation
systems, which allow the translation of Petri net transformations into graph
transformations with equivalent behavior, and, vice versa, the creation of Petri net
transformations from graph transformations. Since this is supposed to work for different
kinds of Petri nets, we propose to define suitable functors, called M-functors,
between different M-adhesive categories and to investigate properties allowing us
the translation and creation of transformations of the corresponding M-adhesive
transformation systems
Modelling and analysing the interactive behaviour of an infusion pump
Get PDFThis paper is concerned with the scaleable and systematic analysis of interactive systems. The motivating problem is the procurement of medical devices. In such situations several different manufacturers offer solutions that support a particular clinical activity. Apart from cost, which is a dominating factor, the variations between devices are relatively subtle and the consequences of particular design features are not clear from manufacturers’ manuals, demonstrations or trial uses. Despite their subtlety these differences can be important to the safety and usability of
the device. The paper argues that formal analysis of the range of offered devices can provide a systematic means of comparison. The paper also explores barriers to the use of such techniques, demonstrating how layers of specification may be used to make it possible to reuse common specification. Infusion pumps provide a motivating example. A specific model is described and analysed and comparison between competitive devices is discussed
Automatically Verifying Railway Interlockings using SAT-based Model Checking
Get PDFIn this paper, we demonstrate the successful application of various SAT-based model checking techniques to verify train control systems. Starting with a propositional model for a control system, we show how execution of the system can be modelled via a finite automaton. We give algorithms to perform SAT-based model checking over such an automaton. In order to tackle state-space explosion we propose slicing. Finally we comment on results obtained by applying these methods to verify two real-world railway interlocking systems
A Symbolic Model Checking Approach to Verifying Satellite Onboard Software
Get PDFThis paper discusses the use of symbolic model checking technology to verify the design of an embedded software control system called attitude and orbit control system (AOCS). This system is mission-critical because it is responsible for maintaining the attitude of the satellite and for performing fault detection, isolation, and recovery decisions of the satellite. An executable AOCS implementation by Space Systems Finland has been provided to us in Ada source code form. In order to use symbolic model checking methods, the Ada implementation of the system was modeled at a quite detailed implementation level using the input language of the symbolic model checker NuSMV 2. We describe the modeling techniques and abstractions used to alleviate the state explosion problem due to handling of timers and the large number of system components controlled by AOCS. The specification of the required system behavior was also provided to us in a form of extended state machine diagrams with prioritized transitions. These diagrams have been translated to a set of temporal logic properties, allowing the piecewise checking of the system behavior one extended state machine transition at a time. We also report on the scalability of symbolic model checking tools for the case study at hand as well as discuss potential topics for future work
Integrating Formal Methods with Informal Digital Hardware Development
Get PDFThis paper presents some results from an industrial project to develop high-integrity digital hardware by integrating formal methods with a more traditional informal approach. The ultimate goal of the project team was to produce sythesisable VHDL that could be proven to meet given requirements for an embedded controller. The burden was on the formal methods experts to integrate themselves into the team. This paper describes the formal approach that was developed as a result