1,720,968 research outputs found
Modelling and Verification of Embedded Systems based on Petri Net oriented Representations
No full textDriven by the demand for more functionality, the complexity involved in the design of embedded systems continues to increase. This has lead to a progressive increase in the amount of control and data flow that current embedded systems need to deal with. This dissertation addresses the interaction between these two domains and investigates its influence on the design of embedded systems, in terms of overall design cost. The first part of this dissertation presents the formalisation of a new design representation, called Dual Flow Net (DFN), which provides a tight control and data flow interaction. This is achieved by means of two new concepts. Firstly, the structure of the new DFN model is formulated employing a tripartite graph, as opposed to previous approaches based on a bipartite graph. Such a structure allows the use of a unique semantics to model the control flow, data flow, and its interactions. Secondly, a marking scheme that captures the changes in the state of the system produced by the separated effects of control and data flow is described. The analysis of behavioural properties using such a marking is proposed, and illustrative examples are given. The second part of this dissertation is concerned with the verification of DFN models through formal methods. A new set of algorithms for the symbolic model checking of DFN models is proposed. Behavioural properties of embedded systems, such as reachability, safety and liveness, are verified, using both Computation Tree Logic (CTL) and Linear Temporal Logic (LTL) formulae. The description of a new estimation method is provided, which is capable of allocating resources to the verification process efficiently, hence dealing with the state explosion problem. The algorithms and estimation method have been validated by examples of varying complexity, ranging from simple systems, in order to understand the modelling and verification principles, up to complex arrangements that depict real-life embedded systems, including an Ethernet coprocessor. The final part of this dissertation investigates the applicability of DFN models to the co-synthesis of hardware/software systems, as a potential application of the new design representation. It has been shown how the DFN model provides a flexible design framework for system-level trade-offs in the generated solution
Transforming Dual Flow Nets into Object Petri Nets
No full textThis paper summarises two approaches, Dual Flow Nets (DFN) and Object Petri Nets (OPN), and offers a translation mechanism between them. While the DFN model tackles the separation of control and data flow computing aspects, the OPN model has a more generalised structure. The aim of this paper is to show how the modelling based on control/data-flow analysis can benefit from an object-based Petri net approach. Tool support and a translation mechanism that is faithful are pesented, giving an extra dimension (hierarchy) to the existing paradigm of control and data flow interacting in a model. Our methodology provides a comprehensive separation of these two parts, which can be used to feed analysis or synthesis tools, while still being able to reason about both parts through formal methods of verification
Object-based Control/Data-flow Analysis
No full textNot only does a clear distinction between control and data flow enhance the readability of models, but it also allows different tools to operate on the two distinct parts of the model. This paper shows how the modelling based on control/data-flow analysis can benefit from an object-based approach. We have developed a translation mechanism that is faithful and gives an extra dimension (hierarchy) to the existing paradigm of control and data flow interacting in a model. Our methodology provides a comprehensible separation of these two parts, which can be used to feed another analysis or synthesis tools, while still being able to reason about both parts through formal methods of verification
Efficient and Flexible Access Control via Jones-Optimal Logic Program Specialisation
No full textWe describe the use of a flexible meta-interpreter for performing access control checks on deductive databases. The meta-program is implemented in Prolog and takes as input a database and an access policy specification. For processing access control requests we specialise the meta-program for a given access policy and database by using the Logen partial evaluation system. The resulting specialised control checking program is dependent solely upon dynamic information that can only be known at the time of actual access request evaluation. In addition to describing our approach, we give a number of performance measures for our implementation of an access control checker. In particular, we show that by using our approach we get flexible access control with virtually no overhead, satisfying the Jones optimality criterion. The paper also shows how to satisfy the Jones optimality criterion more generally for interpreters written in the non-ground representation
Improving Compositional Verification of State-based Models by Reducing Modular Unbalance
No full textCompositional Verification is a viable way to tackle the state explosion problem. However, the decomposition of a system into smaller parts is not a trivial problem, and dividing the specification into modules can be regarded as one of the main issues that concerns a compositional approach. This paper concentrates on the application of compositional verification to state-based models, in order to reduce the number of nodes assigned to memory, thus avoiding state explosion and speeding up the verification. Furthermore, we investigate and propose an estimation method that improves the compositional verification process in modular designs, such that the amount of memory required by the process is minimised. This method has been applied to a real-life embedded system, producing meaningful results without the need of data abstraction
Dual Transitions Petri Net based Modelling Technique for Embedded Systems Specification
No full textThis paper presents a new modelling technique capable of modelling both control and data information using a single unified approach. This is achieved by modifying the classical Petri Net structure, allowing it to have two types of transitions and arcs. As a consequence, loops and conditional operations within complex specifications are easily identified. The system dynamic behaviour is modelled using a new marking scheme of the net consisting of a new element called "value" for data representation in addition to classical tokens used for control purpose. Structural definitions, behavioural rules and graphical representation of the new modelling technique are given. One potential application of the proposed modelling technique is the internal representation of embedded systems specification. Two examples are included illustrating the applicability and efficiency of the proposed modelling technique
Towards Context-aware Testing for Semantic Interoperability on PvC Environments
No full textNew challenges in Software Testing arise from evaluating Pervasive Computing Systems, which are a special type of component-based software. Transparent interconnection of components becomes highly important when users need to switch between operative contexts. Dynamic assembly requires evaluating components to ensure they conform to the updated system’s requirements, and components semantical information could be analysed with a proper Ontology. Thus, our focus is set on Semantic Interoperability. We present an abstract model of an infrastructure integrated with an evaluation process, by applying testing strategies based on contextual information of components and user tasks. A typical case study is used to present both static and dynamic aspects of participating components. To improve this description we show the components’ dynamic interaction by a temporal model from which testing strategies could be more precisely defined and applied
- …
