Search

Software that is used to control machines and robots must be predictable and reliable. Model-Driven Design (MDD) techniques are used to comply with both the technical and business needs. This paper introduces a CSP meta-model that is suitable for these MDD techniques. The meta-model describes the structure of CSP models that are designed; using this meta-model it is possible to use all regular CSP constructs when constructing a CSP model. The paper also presents a new tool suite, called TERRA, based on Eclipse and its frameworks. TERRA contains a graphical CSP model editor (using the new CSP meta-model), model validation tools and code generation tools. The model validation tools check whether the model conforms to the meta-model definition as well as to additional rules. Models without any validation problems result in proper code generation, otherwise the developer needs to address the found problems to be sure code generation will succeed. The code generation tools are able to generate CSPm code that is readable by FDR and to generate C++/LUNA code that is executable on embedded targets. The meta-model and the TERRA tool suite are tested by designing CSP models for several of our laboratory setups. The generated C++/LUNA code for the laboratory setups is able to control them as expected. Additionally, the paper contains an example model containing all supported CSP constructs to show the CSPm code generation results. So it can be concluded that the meta-model and TERRA are usable for these kind of tasks.

The aims of this workshop are to develop a range of interesting practical demonstrators showing the benefits and advantages to systems engineering of Com- municating Process Architectures (CPA). Examples range from essential, basic cases towards the challenging ones. Also, benchmark cases – or cases that are used so often that they grow towards a benchmark, like the commstime example – will be developed.

Timed CSP can be used to model and analyse real-time and concurrent behaviour of embedded control systems. Practical CSP implementations combine the CSP model of a real-time control system with prioritized scheduling to achieve efficient and orderly use of limited resources. Schedulability analysis of a timed CSP model of a system with respect to a scheduling scheme and a particular execution platform is important to ensure that the system design satisfies its timing requirements. In this paper, we propose a framework to analyse schedulability of CSP-based designs for non-preemptive fixed-priority multiprocessor scheduling. The framework is based on the PAT model checker and the analysis is done with dense-time model checking on timed CSP models. We also provide a schedulability analysis workflow to construct and analyse, using the proposed framework, a timed CSP model with scheduling from an initial untimed CSP model without scheduling. We demonstrate our schedulability analysis workflow on a case study of control software design for a mobile robot. The proposed approach provides non-pessimistic schedulability results.

This paper describes and compares five CSP based and two CSP related process-oriented motion control system implementations that are made for our Production Cell demonstration setup. Five implementations are software-based and two are FPGA hardware-based. All implementations were originally made with different purposes and investigating different areas of the design space for embedded control software resulting in an interesting comparison between approaches, tools and software and hardware implementations. Common for all implementations is the usage of a model-driven design method, a communicating process structure, the combination of discrete event and continuous time and that real-time behaviour is essential. This paper shows that many small decisions made during the design of all these embedded control software implementations influence our route through the design space for the same setup, resulting in seven different solutions with different key properties. None of the implementations is perfect, but they give us valuable information for future improvements of our design methods and tools.

This paper presents two algorithms for analysing gCSP models in order to improve their execution performance. Designers tend to create many small separate processes for each task, which results in many (resource intensive) context switches. The research challenge is to convert the model created from a design point of view to models which have better performance during execution, without limiting the designers in their ways of working. The first algorithm analyses the model during run-time execution in order to find static sequential execution traces that allow for optimisation. The second algorithm analyses the gCSP model for multi-core execution. It tries to find a resource-efficient placement on the available cores for the given target systems. Both algorithms are implemented in two tools and are tested. We conclude that both algorithms complement each other and the analysis results are suitable to create optimised models.

We prove the correctness of a two-way sliding window protocol with piggybacking, where the acknowledgments of the latest received data are attached to the next data transmitted back into the channel. The window size of both parties are considered to be finite, though they can be of different sizes. We show that this protocol is equivalent (branching bisimilar) to a pair of FIFO queues of finite capacities. The protocol is first modeled and manually proved for its correctness in the process algebraic language of muCRL. We use the theorem prover PVS to formalize and to mechanically prove the correctness. This implies both safety and liveness (under the assumption of fairness).

This paper introduces SystemCSP – a design methodology based on a visual notation that can be mapped onto CSP expressions. SystemCSP is a graphical design specification language aimed to serve as a basis for the specification of formally verifiable component-based designs of distributed real-time systems. It aims to be a graphical formalism that covers various aspects needed for the design of distributed real-time systems in single framework. Keywords. CSP, Formal methods, Graphical modeling

SystemCSP is a graphical modeling language based on both CSP and concepts of component-based software development. The component framework of SystemCSP enables specification of both interaction scenarios and relative execution ordering among components. Specification and implementation of interaction among participating components is formalized via the notion of interaction contract. The used approach enables incremental design of execution diagrams by adding restrictions in different interaction diagrams throughout the process of system design. In this way all different diagrams are related into a single formally verifiable system. The concept of reusable formally verifiable interaction contracts is illustrated by designing set of design patterns for typical fault tolerance interaction scenarios. Keywords. SystemCSP, CSP, components, contracts, contexts, fault tolerance, design patterns, formal methods, graphical modeling, simulation, hierarchical verification.