• Safe CCSL Specifications and M...

Treffer: Safe CCSL Specifications and Marked Graphs

Title:
Safe CCSL Specifications and Marked Graphs
Authors:
Mallet, Frédéric, Millo, Jean-Vivien, de Simone, Robert
Contributors:
Models and methods of analysis and optimization for systems with real-time and embedding constraints (AOSTE), Centre Inria d'Université Côte d'Azur, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED), Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (1965 - 2019) (UNS)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UniCA)-Université Nice Sophia Antipolis (1965 - 2019) (UNS)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UniCA)-Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (1965 - 2019) (UNS)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UniCA)-Université Nice Sophia Antipolis (1965 - 2019) (UNS)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UniCA), Roncken, Marly and Talpin, Jean-Pierre, European Project: 269362,ARTEMIS-2010-1,ARTEMIS-2010-1,PRESTO(2011)
Source:
MEMOCODE - 11th IEEE/ACM International Conference on Formal Methods and Models for Codesign. :157-166
Publisher Information:
CCSD; IEEE CS, 2013.
Publication Year:
2013
Collection:
collection:UNICE
collection:CNRS
collection:INRIA
collection:INRIA-SOPHIA
collection:INRIA-ROCQ
collection:I3S
collection:INRIASO
collection:INRIA_TEST
collection:AOSTE
collection:TESTALAIN1
collection:INRIA2
collection:UNIV-COTEDAZUR
collection:INRIA-300009
collection:TEST-NICE
Subject Terms:
ACM: D.: Software, D.2: SOFTWARE ENGINEERING, D.2.2: Design Tools and Techniques, ACM: F.: Theory of Computation, F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES, F.4.1: Mathematical Logic, F.4.1.3: Logic and constraint programming, [INFO.INFO-ES]Computer Science [cs], Embedded Systems
Subject Geographic:
Portland, United States
Original Identifier:
HAL: hal-00913962
Document Type:
Konferenz conferenceObject<br />Conference papers
Language:
English
Relation:
info:eu-repo/grantAgreement//269362/EU/ImProvements of industrial Real Time Embedded SysTems devel0pment process/PRESTO
Access URL:
https://inria.hal.science/hal-00913962
https://inria.hal.science/hal-00913962v1/document
https://inria.hal.science/hal-00913962v1/file/memocodePub.pdf
Rights:
info:eu-repo/semantics/OpenAccess
Accession Number:
edshal.hal.00913962v1
Database:
HAL

Weitere Informationen

The Clock Constraint Specification Language (CCSL) proposes a rich polychronous time model dedicated to the specification of constraints on logical clocks: i.e., sequences of event occurrences. A priori independent clocks are progressively constrained through a set of clock operators that define when an event may occur or not. These operators can be described as labeled transition systems that can potentially have an infinite number of states. A CCSL specification can be scheduled by performing the synchronized product of the transition systems for each operator. Even when some of the composed transition systems are infinite, the number of reachable states in the product may still be finite: the specification is safe. The purpose of this paper is to propose a sufficient condition to detect that the product is actually safe. This is done by abstracting each CCSL constraint (relation and expression) as a marked graph. Detecting that some specific places, called counters, in the resulting marked graph are safe is sufficient to guarantee that the composition is safe.