The polychronous or multi-clock paradigm is adequate to model large distributed systems where achieving a full timed synchronization is not only very costly but also often not necessary. It concerns systems made of a set of components with loose synchronization constraints. We study an approach where those components are orchestrated using...
-
June 26, 2024 (v1)Journal articleUploaded on: October 24, 2024
-
December 11, 2018 (v1)Conference paper
Scheduling is a central yet challenging problem in real-time embedded systems. The Clock Constraint Specification Language (CCSL) provides a formalism to specify logical constraints of events in real-time embedded systems. A prerequisite for the events is that they must be schedulable under constraints. That is, there must be a schedule which...
Uploaded on: December 4, 2022 -
October 2020 (v1)Journal article
International audience
Uploaded on: December 4, 2022 -
May 2016 (v1)Journal article
本文为分布式语言提出一个表达能力较强的模型-同步自动机的参数化网络。 通过定义开放式自动机给出了此模型的行为语义, 并在此基础上给出了一种特殊的等价关系--规范假设互模拟等价。 我们讨论了这种等价关系在规范假设条件下的可复合性和可判定性。
Uploaded on: February 28, 2023 -
November 6, 2015 (v1)Conference paper
The Clock Constraint Specification Language (ccsl) is a language to specify logical and timed constraints between logical clocks. Given a set of clock constraints specified in ccsl, formal analysis is preferred to check if there exists a schedule that satisfies all the constraints, if the constraints are valid or not, and if the constraints...
Uploaded on: February 28, 2023 -
September 15, 2017 (v1)Book
The 11th Theoretical Aspects of Software Engineering Conference (TASE 2017) will be held in Nice, France on September 13-15, 2017. TASE is an international symposium that aims to bring together researchers and developers from academia and industry with interest in the theoretical aspects of software engineering. Modern society is increasingly...
Uploaded on: February 28, 2023 -
March 2018 (v1)Journal article
The UML profile for Modeling and Analysis of Real-Time and Embedded systems (MARTE) is used to design and analyze real-time and embedded systems. The Clock Constraint Specification Language (ccsl) is a companion language for MARTE. It introduces logical clocks as first class citizens as a way to formally specify the expected behavior of models...
Uploaded on: December 4, 2022 -
June 6, 2016 (v1)Conference paper
In this paper, we provide a theory for the operators composing concurrent processes. Open pNets (parameterised networks of synchronised automata) are new semantic objects that we propose for defining the semantics of composition operators. This paper defines the operational semantics of open pNets, using "open transitions" that include symbolic...
Uploaded on: February 28, 2023 -
January 30, 2021 (v1)Report
Open Automata (OA) are symbolic and parameterized models for open concurrent systems. Here open means partially specified systems, that can be instantiated or assembled to build bigger systems. An important property for such systems is "compositionality", meaning that logical properties, and equivalences, can be checked locally, and will be...
Uploaded on: December 4, 2022 -
November 20, 2014 (v1)Report
This article studies Parameterised Networks of Automata (pNets) from a theoretical perspective. We illustrate the expressiveness of pNets by showing how to express a wide range of classical constructs of (value-passing) process calculi, but also how we can easily express complex interaction patterns used in modern distributed systems. Our...
Uploaded on: March 25, 2023 -
November 14, 2016 (v1)Conference paper
MARTE (abbreviated for Modeling and Analysis of Real-Time and Embedded systems) is a UML profile which provides a generalmodeling framework to design and analyze real-time embedded systems. CCSL (abbreviated for Clock Constraint Specification Language) is aformal language companion to MARTE, used to specify the constraints between the...
Uploaded on: February 28, 2023 -
April 2016 (v1)Report
In this paper, we provide a theory for the operators composing concurrent processes. Open pNets (parameterised networks of synchronised automata) are new semantic objects that we propose for defining the semantics of composition operators. This paper defines the operational semantics of open pNets, using ``open transitions'' that include...
Uploaded on: February 28, 2023 -
2015 (v1)Conference paper
This article studies Parameterised Networks of Automata (pNets) from a theoretical perspective. We illustrate the expressiveness of pNets by showing how to express a wide range of classical constructs of (value-passing) process calculi, but also how we can easily encode complex interaction patterns used in modern distributed systems. Our...
Uploaded on: March 25, 2023 -
March 9, 2020 (v1)Conference paper
The Clock Constraint Specification Language (CCSL) is a logical time based modeling language to formalize timing behaviors of real-time and embedded systems. However, it cannot capture timing behaviors that contain uncertainties, e.g., uncertainty in execution time and period. This limits the application of the language to real-world systems,...
Uploaded on: December 4, 2022 -
July 15, 2018 (v1)Conference paper
Open pNets are used to model the behaviour of open systems , both synchronous or asynchronous, expressed in various calculi or languages. They are endowed with a symbolic operational semantics in terms of so-called "Open Automata". This allows us to check properties of such systems in a compositional manner. We implement an algorithm computing...
Uploaded on: December 4, 2022 -
April 9, 2019 (v1)Conference paper
The Clock Constraint Specification Language (CCSL) is a formalism for specifying logical-time constraints on events for the design of real-time embedded systems. A central verification problem of CCSL is to check whether events are schedulable under logical constraints. Although many efforts have been made addressing this problem, the problem...
Uploaded on: December 4, 2022 -
June 2018 (v1)Report
Open pNets are used to model the behaviour of open systems, both synchronousor asynchronous, expressed in various calculi or languages. They are endowed with a symbolicoperational semantics in terms of so-called "Open Automata". This allows us to check properties ofsuch systems in a compositional manner. We implement an algorithm computing...
Uploaded on: December 4, 2022 -
May 1, 2023 (v1)Journal article
The Clock Constraint Specification Language (CCSL) has been widely acknowledged as a promising system-level specification for the modeling and analysis of timing behaviors of real-time and embedded systems. However, along with the increasing complexity of modern systems coupled with strict time-to-market constraints, it becomes more and more...
Uploaded on: September 5, 2023 -
December 7, 2021 (v1)Conference paper
The Clock Constraint Specification Language (CCSL) has become popular for modeling and analyzing timing behaviors of real-time embedded systems. However, it is difficult for requirement engineers to accurately figure out CCSL specifications from natural language-based requirement descriptions. This is mainly because: i) most requirement...
Uploaded on: December 3, 2022 -
August 2009 (v1)Journal article
Polarized epithelial cells contain apical and basolateral surfaces with distinct protein compositions. To establish and maintain this asymmetry, newly made plasma membrane proteins are sorted in the trans Golgi network for delivery to apical or basolateral surfaces. Signals for basolateral sorting are generally located in the cytoplasmic domain...
Uploaded on: December 3, 2022 -
June 2, 2019 (v1)Conference paper
The Clock Constraint Specification Language (CCSL) has been widely investigated in verifying causal and temporal timing behaviors of real-time embedded systems. However, due to limited expertise in formal modeling, it is difficult for requirement engineers to completely and accurately derive CCSL specifications from natural language-based...
Uploaded on: December 4, 2022 -
June 12, 2023 (v1)Journal article
As a promising requirement-level specification language for timing behavior modeling, the Clock Constraint Specification Language (CCSL) has become popular in the model-driven design community for safety-critical embedded systems. However, due to the skyrocketing design complexity, in practice, it is hard for requirement engineers to accurately...
Uploaded on: September 5, 2023 -
August 2024 (v1)Journal article
Dealing with the ever-growing complexity of railway systems requires scalable approaches for detecting inconsistent safety requirements in practice. Despite significant efforts to automate the requirements consistency detection, current inconsistency analysis techniques of railway safety requirements still suffer from scalability issues. This...
Uploaded on: October 24, 2024