Analyzing and Simulating Time Descriptions from UML/MARTE CCSL
The complexity of modern embedded systems makes it inevitable to consider higher abstraction levels in the design process to overcome problems in acceptable time and effort. In higher abstraction levels, the utilization of functional requirements is quite
- PDF / 254,376 Bytes
- 3 Pages / 476.221 x 680.315 pts Page_size
- 68 Downloads / 159 Views
Abstract. The complexity of modern embedded systems makes it inevitable to consider higher abstraction levels in the design process to overcome problems in acceptable time and effort. In higher abstraction levels, the utilization of functional requirements is quite advanced, while the utilization of non-functional requirements like timing still is an open problem. We aim to address this problem utilizing the timing definitions from UML/MARTE CCSL. Keywords: CCSL, UML, MARTE, SystemC, Formal Methods
1
Introduction
Modern embedded systems are growing to a huge complexity, making classical design tasks error-prone and time-consuming. As a consequence, novel design flows introduced several abstraction levels to overcome this problem. At this stage, the classical level of highest abstraction is the Electronic Systems Level (ESL), where SystemC and other high-level programming languages are used to describe the system. But still, a big gap remains between textual specification and ESL. In the last decade, modeling languages like the Unified Modeling Language (UML, [2]) provided a “bridge” between the given specification and its initial implementation [4]. In the design of embedded and cyber-physical systems, particularly the Modeling and Analysis of Real-time and Embedded systems profile (MARTE, [1]) finds considerable attention. In this field, the utilization of non-functional requirements like timing is still an open problem. MARTE provides a special language for timing specification: the Clock Constraint Specification Language (CCSL), which relies on describing clocks and instants. In our project we are going to utilize this language for classical design tasks such as verification or code-generation.
2
Design and More – A Generic Representation of CCSL
To utilize the textual CCSL specification, we introduce a generic automaton representation of it. A lot of approaches have already been proposed to directly
This work was supported by the Graduate School SyDe, funded by the German Excellence Initiative within the University of Bremen’s institutional strategy.
R. Drechsler, U. Kühne (eds.), Formal Modeling and Verification of Cyber-Physical Systems, DOI 10.1007/978-3-658-09994-7_17, © Springer Fachmedien Wiesbaden 2015
294
J. Peters g : (cA = 2) ∨ ¬dA u : (cA = 0) ∧ (dA = true) {B}
A isPeriodicOn B period 2 . 0 ; (a) CCSL constraints
g : cA < 2 u : cA + +
{A,B}
g : cA < 2 u : cA + +
V0 = (cA = 0, dA = false)
(b) Corresponding automaton
Fig. 1. Generic representation of CCSL constraints
transform the CCSL constraints to input for certain model checkers [5] or to ESL descriptions [3]. We transform it to a more generic representation which can be used for several tasks at the same time. The main concept of our approach is the ticking set, which is the set of clocks c ∈ C ticking in one simulation step. All clock behavior can be modeled as a movement between these ticking sets, making the ticking sets states and the movement between them the transitions. These transitions can be restricted according to the CCSL const
Data Loading...
