| 1: | The Automated Verification of Timewise Refinement |
| | Bill Roscoe |
| | Paper: PDF |
| Abstract: While Hoare's CSP models reactive systems without assigning an exact time to events,
Timed CSP records the exact times as non-negative reals. Timed CSP therefore provides a more exact semantics of systems, but
it still makes sense to ask whether a timed process satisfies an untimed specification. Indeed the question of whether such
specifications are satisfied often reduces to the timing details of the implementation. Schneider showed how this could be
understood at an abstract level via the concept of timewise refinement. The recent implementation of Timed CSP in the CSP
refinement checker FDR (using Ouaknine's theory of digitisation) has at last provided the framework for automatic timewise
refinement. In this paper we show how to do this, discovering that it is subtle because of the need to reconcile infinite
behaviours with finite ones. |
| 2: | Runtime Quantitative Verification: Applications and Research Challenges |
| | Radu Calinescu |
| | Paper: PDF |
| Abstract: A growing number of software and embedded systems are expected to adapt continually to changes in the environments they operate in. Many of these systems are deployed in safety-critical and business-critical applications from domains including healthcare, finance and defence, and must comply with strict dependability and performance requirements. To achieve such compliance, formal approaches traditionally employed in the design of critical systems must also be used during their operation. This talk will describe how a formal approach termed quantitative verification can be exploited in a runtime setting. Quantitative verification is a mathematically based technique for the modelling and analysis of the correctness, performance and reliability of systems that exhibit stochastic behaviour. The talk will present several successful runtime applications of the technique, and will discuss the research challenges that must be addressed in order to extend its applicability to additional runtime scenarios. |
| 3: | On the Technological and Methodological Concepts
of Federated Embedded Systems |
| | Avenir Kobetski, Jakob Axelsson |
| | Paper: PDF |
| | Abstract: Traditionally embedded systems are developed with a specific control task in mind, and are able to affect only a
limited set of actuators, based on measurements from a limited set of sensors. With the arrival of cheap and efficient
communication technology, this traditional picture is starting to change. It is our belief that future embedded systems will interact
with each other, forming federations to provide new emergent services to their users. With this in mind, a pre-study was
performed to discern the main concepts of such federations and the related challenges that need to be addressed. This has led to
two parallel research directions, presented in this paper. One is focusing on the enabling technology that is needed for dynamic
creation of new types of federations, while the other deals with the methodological concepts for creation of ecosystems in which
federations of embedded systems can be dynamically formed. |
| 4: | A Roadmap Towards Integrated CPS Development Environments
|
| | Jad El-khoury, Fredrik Asplund, Matthias Biehl, Frederic Loiret, Martin Törngren |
| | Paper: PDF |
| | Abstract: Cyber Physical System (CPS) development is highly heterogeneous, involving many stakeholders, each of
which interacts with its development artifacts through a variety of tools, and within several engineering processes.
Successful CPS development requires these tools to be well-integrated into a Development Environment (DE) in order to
support its many stakeholders and processes. In this paper we identify the main
challenges facing DE development for CPSs, and presents a roadmap to meet these challenges. We here take
the position that focus should be redirected from trying to achieve a single, one-size-fits-all solution to such a
heterogeneous problem. Instead, focus should be placed on supporting the development of highly-customized
DEs, which readily can be applied to industrial development. Such a highly-customized DE should fit the
needs of a particular development organization, while at the same time taking advantage of relevant standardization efforts. |
| 5: | Engineering of Cyber-Physical Systems
|
| | María Victoria Cengarle |
| | Paper: PDF |
| | Abstract: The present work reflects on the drivers
and barriers of Cyber-Physical Systems with focus on the challenges associated with
their engineering. |
| 6: | Towards autonomous embedded systems |
| | Sagar Behere, Martin Törngren, Jad El-khoury, DeJiu Chen |
| | Paper: PDF |
| | Abstract: Machines incorporating embedded systems display a trend towards increasing autonomy. In this position paper,
we outline an approach for introducing autonomy in embedded system architectures. The approach involves the creation of an
artificial consciousness within the machine. We propose that the artificial consciousness may be represented in the form of domain
specific reference architectures. We illustrate the approach with the aid of a validated reference architecture for cooperative
driving. |
| 7: | Towards Dynamic Deployment Calculation for
Extensible Systems using SMT-Solvers |
| | Klaus Becker, Sebastian Voss |
| | Paper: PDF |
| | Abstract: uring design of distributed embedded systems, the determination of the deployment of software components
to execution units is a crucial subtask of the design space exploration. In static systems, the deployment can be determined
at design time. However, in many cases it is desired to add new functional features into existing systems after sale. In this case,
new software components have to be integrated into the former system and hence, into an existing deployment.
We aim in a self-configuring system that ensures the integrity of the integration of new components autonomously. Our pro-
posed process of integrating new components into a given system consists of several steps intended to be applied at run-time while
the system is in operation. Beside others, the process includes a logical admission control, followed by a self-configuration of the
system.
In this paper, we focus on extending an existent deployment during the self-configuration phase incrementally. We sketch a
mechanism that extends existing deployments with additional components in an efficient way by using SMT-solvers. We also
present an example that demonstrates how these solutions are calculated based on given deployment-constraints. |
| 8: | Synchronous Specialization of Alf for Cyber-Physical Systems
|
| | Alessandro Gerlinger Romero, Klaus Schneider, Maurício Gonçalves Vieira Ferreira |
| | Paper: PDF |
| | Abstract: Systems engineers use SysML as a vendor-independent language to model Cyber-Physical Systems.
However, SysML does not provide an executable form to define behavior but this is needed to detect critical issues as soon as
possible. Alf integrated with SysML can offer some degree of precision. In this paper, we present an Alf specialization that
introduces the synchronous paradigm to SysML, through definition of not explicitly constrained semantics: timing,
concurrency, and inter-object communication. The Smart Parking system, a well-known cyber-physical system, was
selected to evaluate this specialization. Our initial results show that the proposed specialization does not add complexity to the
task of modeling using SysML, and enables concise and precise behavioral definitions. |
| 9: | Robotic car-like vehicles: a case study for
cyberphysical systems
|
| | Federico Moro, Tizar Rizano, Daniele Fontanelli, Luigi Palopoli |
| | Paper: PDF
|
| | Abstract: The objective of this paper is to present a realistic case-study for the development of cyberphysical systems.
The level of complexity has been chosen as a compromise between featuring many of the requirements of future cyberphysical systems and being easy to
replicate with a moderate effort for all researchers interested to use it as a benchmark for their methodologies. |
