Early design artifacts of embedded systems, such as architectural models, represent convenient abstractions for reasoning about a system's structure and functionality. One such example is the Electronic Architecture and Software Tools-Architecture Description Language (EAST-ADL), a domain-specific architectural language that targets the automotive industry. EAST-ADL is used to represent both hardware and software elements, as well as related extra-functional information (e.g., timing properties, triggering information, resource consumption). Testing architectural models is an important activity in engineering large-scale industrial systems, which sparks a growing research interest. The main contributions of this paper are: (i) an approach for creating energy-related mutants for EAST-ADL architectural models, (ii) a method for overcoming the equivalent mutant problem (i.e., the problem of finding a test case which can distinguish the observable behavior of a mutant from the original one), (iii) a test generation approach based on UPPAAL Statistical Model Checker (SMC), and (iv) a test selection criteria based on mutation analysis using our MATS tool.
Linear references are guaranteed to be free from aliases. This is a strong property that simplifies reasoning about programs and enables powerful optimisations, but it is also a property that is to ...
Modeling is a well-established practice in the development of big and complex software systems. Domain Specific Modeling Languages (DSMLs) are a technique used for specifying such systems in an abstract way. These languages define the structure, semantics and constraints for models related to the same application domain. The models created with DSMLs are then interconnected or related to one another. Among the reasons for tailoring a language to the problem space is their better understandability by domain experts, capacity for high-level abstraction, and user friendliness. However, the use of DSMLs (like the use of types in general) does not shield the produced software from bugs or man-made mistakes. Software failures may still occur on complex systems due to a variety of reasons such as design errors, hardware breakdown or network problems. Ruling out these failures requires that verification methods that guarantee correct execution even in corner cases are integrated into the development process. We previously presented our ideas for integrating specifications tighter with the model [4]. We improve on our realisation in the context of behavioural models for embedded systems [6], and now tackle modelling and specification of a distributed system. LEGO MindStorm R © robots serve as the platform for a small case study.
Hierarchical scheduling frameworks (HSFs) are a means for composing complex real-time embedded systems from independently developed and analyzed applications. To support multiple modes in a two-lev ...
Many software systems adopt isolation mechanisms of modern processors as software security building blocks. Reasoning about these building blocks means reasoning about elaborate assembly code, which can be very complex due to the loose structure of the code. A way to overcome this complexity is giving the code a more structured semantics. This paper presents one such semantics, namely a fully abstract trace semantics, for an assembly language enhanced with protection mechanisms of modern processors. The trace semantics represents the behaviour of protected assembly code with simple abstractions, unburdened by low-level details, at the maximum degree of precision. Additionally, it captures the capabilities of attackers to protected software and simplifies providing a secure compiler targeting that language.
We present a method for polyhedral abstract interpretation which derives fully bounded polyhedra for every step in the analysis. Contrary to classical polyhedral analysis, this method is sound for ...
European hospitals are being placed under growing pressure to deliver efficiency gains due to an increasing elderly population and ever tighter financial constraints. A significant proportion of the treatment performed relies on the adaptive application of various intravenous medicine which is mostly in liquid form and which is prepared in central pharmacies serving a number of departments. Due to strict safety requirements within pharmacies, the process of preparation of fluid medicine for intravenous use is; labour intensive, inefficient[3], error-prone[1, 6] and poses health risks to medical staff. Current product preparation workflows rely on production techniques largely abandoned by other industries; including duplicating inventory, inflexible batch processing, and over production where doses are often prepared in anticipation of a need or demand that may end up not being realised which contributes to waste[7]. A solution to these issues has been sought in the automation of the medication management and dispensing processes. Deployment of systems for this purpose has delivered significant improvements in safety for both staff and patients[2, 10], and new pharmacy capabilities such as customised medicine have become feasible[2]. However, the technology has proven disruptive to traditional pharmacy processes and many potential efficiency gains have yet to be realised.
In this paper we investigate multicore parallelism in the context of functional programming by means of two quantifier-elimination procedures for Presburger Arithmetic: one is based on Cooper's algorithm and the other is based on the Omega Test.We first develop correct-by-construction prototype implementations in a functional programming language. Thereafter, the parallelism inherent in the decision procedures is analyzed using the Directed Acyclic Graph (DAG) model of multicore parallelism. In the step from a DAG model to a parallel implementation, the parallel implementation is optimized taking into account negative factors such as cache misses, garbage collection and overhead due to task creations, because such factors may introduce sequential bottlenecks with severe consequences for the parallel efficiency.The experiments were conducted using the functional programming language F# and .NET platform executing on an 8-core machine. A speedup of approximately 4 was obtained for Cooper's algorithm and a speedup of approximately 6 was obtained for the exact-shadow part of the Omega Test.The considered procedures are complex, memory-intense algorithms on huge formula trees and the case study reveals more general applicable techniques and guideline for deriving parallel algorithms from sequential ones in the context of data-intensive tree algorithms. The obtained insights should apply for any strict and impure functional programming language.Furthermore, the results obtained for the exact-shadow elimination procedure have a wider applicability because they can directly be transferred to the Fourier-Motzkin elimination method. (C) 2014 Elsevier Inc. All rights reserved.
Delta-oriented programming is a compositional approach to flexibly implementing software product lines. A product line is represented by a code base and a product line declaration . The code base consists of a set of delta modules specifying modifications to object-oriented programs. A particular product in a delta-oriented product line is generated by applying the modifications contained in the suitable delta modules to the empty program. The product-line declaration provides the connection of the delta modules with the product features. This separation increases the reusability of delta modules. In this paper, we provide a foundation for compositional type checking of delta-oriented product lines of Java programs by presenting a minimal core calculus for delta-oriented programming. The calculus is equipped with a constraint-based type system that allows analyzing each delta module in isolation, such that the results of the analysis can be reused. By relying only on the analysis results for the delta modules and on the product line declaration, it is possible to establish whether all the products of the product line are well typed according to the fragment of the Java type system modeled by the calculus.
Abstract We present the ongoing work on the pathway analysis of a stochastic calculus. Firstly we present a particular stochastic calculus that we have chosen for our modeling - the Interactive Markov Chains calculus, IMC for short. After that we specify a few restrictions that we have introduced into the syntax of IMC in order to make our analysis feasible. Finally we describe the analysis itself together with several theoretical results that we have proved for it. The IMC calculus has been introduced by Holger Hermanns in the 90’s as an orthogonal extension of Continuous Time Markov Chains (CTMC) and a process algebra (see [BH01]). We have adopted the syntax of IMC with a few minor changes (see Table 1). Small Latin letters denote actions that IMC processes are able to execute, capital Latin letters indicate process identifiers and Greek letters correspond to positive real numbers standing for delays during which IMC processes are stuck, i.e. do nothing. Delay durations are not fixed but are exponentially distributed with rates equal to the corresponding numbers. If the rate of some delay is equal to λ , then it’s average duration will be 1 /λ and it’s variation - 1 /λ 2 . One difference with respect to [BH01] is that all summands in the sum construct are ”guarded” either by actions or delay rates (see rule (2) in the Table 1). This is why we use the name guarded IMC or IMC G . Another difference is that all actions and delay rates are decorated with labels from a predefined label set. Labels do not have any semantic meaning but are useful for our analysis.
We present a model of the LMAC protocol for wireless sensor networks in order to analyse collision probabilities for nodes selecting a time slot. We consider fully connected topologies consisting of 3 and 4 nodes, and use probabilistic Uppaal (Uppaal PRO 0.2) for modelling and analysis. The results show that if the waiting time of nodes is increased before the selection of a time slot then the number of collisions decrease and vice versa. However, the results, which are exact due to the model checking technique, indicates that there is only a small loss by using optimistic wait times. This confirms the previously known results which have been reached through simulations. Based on our analysis results, we propose an optimistic choice of a network set-up depending on the probability of waiting times. Besides this, based on the probability of collisions we compare the results of the number of nodes to the number of time slots and suggest a network model for better performance and reduced cost.
