Search

The UML Profile for Modeling and Analysis of Real-Time and Embedded systems promises a general modeling framework to design and analyze systems. Lots of works have been published on the modeling capabilities offered by MARTE, much less on available verification techniques. The Clock Constraint Specification Language (CCSL), first introduced as a companion language for MARTE, was devised to offer a formal support to conduct causal and temporal analysis on MARTE models. This work relies on a state-based semantics for CCSL to establish correctness properties on MARTE/CCSL specifications. We propose and compare two different techniques to build the state-space of a specification. One is an extension of some previous work and is based on extended finite state machines. It relies on integer linear programming to solve the constraints and reduce the state-space. The other one is based on an intentional representation and uses pure Boolean abstractions but offers no guarantee to terminate when the specification is not safe. The approach is illustrated on one simple example where the architecture plays an important role. We describe a process where the logical description of the application is progressively refined to take into account the execution platform through allocation. [ABSTRACT FROM AUTHOR]

We propose a general method to characterize and synthesize correctness-preserving asynchronous wrappers for synchronous processes on a globally asynchronous locally synchronous (GALS) architecture. While a synchronous process may rely on the absence of a signal to trigger a reaction, sensing absence in an asynchronous environment may be unfeasible due to uncontrolled communication latencies. A simple and common solution is to systematically encode and send absence notifications, but it is unduly expensive at run-time. Instead, our approach is based on the theory of weakly endochronous systems, which defines the largest sub-class of synchronous systems where (possibly concurrent) asynchronous evaluation is faithful to the original (synchronous) specification. Our method considers synchronous processes or modules that are specified by synchronization constraints expressed in a high-level multi-clock synchronous reactive formalism. The algorithm uses a compact representation of the abstract synchronization configurations of the analyzed process and determines a minimal set of synchronization patterns generating by union all its possible reactions. A specification is weakly endochronous if and only if these generators do not need explicit absence information. In this case, the set of generators can directly be used to synthesize the concurrent asynchronous multi-rate wrapper of the process. [ABSTRACT FROM AUTHOR]