scholarly journals Hybrid SynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL

2021 ◽  
pp. 491-504
Author(s):  
Jaehun Lee ◽  
Sharon Kim ◽  
Kyungmin Bae ◽  
Peter Csaba Ölveczky
Keyword(s):  
Formal Analysis ◽  
Cyber Physical Systems ◽  
Modeling Language ◽  
Analysis Tool ◽  
Physical Systems ◽  
Complex Control ◽  
Control Programs ◽  
Network Delays ◽  
Execution Times

AbstractWe present the $$\textsc {Hybrid}\textsc {Synch}\textsc {AADL}$$ H Y B R I D S Y N C H AADL modeling language and formal analysis tool for virtually synchronous cyber-physical systems with complex control programs, continuous behaviors, bounded clock skews, network delays, and execution times. We leverage the Hybrid PALS equivalence, so that it is sufficient to model and verify the simpler underlying synchronous designs. We define the $$\textsc {Hybrid}\textsc {Synch}\textsc {AADL}$$ H Y B R I D S Y N C H AADL language as a sublanguage of the avionics modeling standard AADL for modeling such designs in AADL, and demonstrate the effectiveness of $$\textsc {Hybrid}\textsc {Synch}\textsc {AADL}$$ H Y B R I D S Y N C H AADL on a number of applications.

scholarly journals Deriving Specifications of Control Programs for Cyber Physical Systems

2019 ◽  
Vol 63 (5) ◽  
pp. 774-790
Author(s):  
Alan Burns ◽  
Ian J Hayes ◽  
Cliff B Jones
Keyword(s):  
Physical Environment ◽  
Control Program ◽  
Cyber Physical Systems ◽  
Physical Systems ◽  
Control Programs ◽  
Use Of Time ◽  
Temporal Properties ◽  
Physical Components

Abstract Cyber physical systems (CPS) exist in a physical environment and comprise both physical components and a control program. Physical components are inherently liable to failure and yet an overall CPS is required to operate safely, reliably and cost effectively. This paper proposes a framework for deriving the specification of the software control component of a CPS from an understanding of the behaviour required of the overall system in its physical environment. The two key elements of this framework are (i) an extension to the use of rely/guarantee conditions to allow specifications to be obtained systematically from requirements (as expressed in terms of the required behaviour in the environment) and nested assumptions (about the physical components of the CPS); and (ii) the use of time bands to record the temporal properties required of the CPS at a number of different granularities. The key contribution is in combining these ideas; using time bands overcomes a significant drawback in earlier work. The paper also addresses the means by which the reliability of a CPS can be addressed by challenging each rely condition in the derived specification and, where appropriate, improve robustness and/or define weaker guarantees that can be delivered with respect to the corresponding weaker rely conditions.

scholarly journals A GRL-compliant iStar extension for collaborative cyber-physical systems

2021 ◽  
Author(s):  
Marian Daun ◽  
Jennifer Brings ◽  
Lisa Krajinski ◽  
Viktoria Stenkova ◽  
Torsten Bandyszak
Keyword(s):  
Case Studies ◽  
Cyber Physical Systems ◽  
Modeling Language ◽  
Abstract Syntax ◽  
Goal Modeling ◽  
Physical Systems ◽  
Modeling Approaches ◽  
Concrete Syntax ◽  
The Individual ◽  
Do So

AbstractCollaborative cyber-physical systems are capable of forming networks at runtime to achieve goals that are unachievable for individual systems. They do so by connecting to each other and exchanging information that helps them coordinate their behaviors to achieve shared goals. Their highly complex dependencies, however, are difficult to document using traditional goal modeling approaches. To help developers of collaborative cyber-physical systems leverage the advantages of goal modeling approaches, we developed a GRL-compliant extension to the popular iStar goal modeling language that takes the particularities of collaborative cyber-physical systems and their developers’ needs into account. In particular, our extension provides support for explicitly distinguishing between the goals of the individual collaborative cyber-physical systems and the network and for documenting various dependencies not only among the individual collaborative cyber-physical systems but also between the individual systems and the network. We provide abstract syntax, concrete syntax, and well-formedness rules for the extension. To illustrate the benefits of our extension for goal modeling of collaborative cyber-physical systems, we report on two case studies conducted in different industry domains.

scholarly journals Formal requirements modeling for cyber-physical systems engineering: an integrated solution based on FORM-L and Modelica

2021 ◽  
Author(s):  
Daniel Bouskela ◽  
Alberto Falcone ◽  
Alfredo Garro ◽  
Audrey Jardin ◽  
Martin Otter ◽  
...  
Keyword(s):  
Systems Engineering ◽  
Cyber Physical Systems ◽  
Modeling Language ◽  
Design Development ◽  
High Lift ◽  
Air Conditioning System ◽  
Physical Systems ◽  
Requirements Modeling ◽  
System Requirements ◽  
Formal Requirements

AbstractThe increasing complexity of cyber-physical systems (CPSs) makes their design, development and operation extremely challenging. Due to the nature of CPS that involves many heterogeneous components, which are often designed and developed by organizations belonging to different engineering domains, it is difficult to manage, trace and verify their properties, requirements and constraints throughout their lifecycle by using classical techniques. In this context, the paper presents an integrated solution to formally define system requirements and automate their verification through simulation. The solution is based on the FOrmal Requirements Modeling Language and the Modelica language. The solution is exemplified through two case studies concerning a Trailing-Edge High-Lift system and a Heating, Ventilation and Air Conditioning system.

Sign in / Sign up

Export Citation Format

Share Document