SMT-based Probabilistic Analysis of Timing Constraints in Cyber-Physical Systems

Eun-Young Kang*, Li Huang

*Kontaktforfatter for dette arbejde

Publikation: Konferencebidrag uden forlag/tidsskriftPosterForskningpeer review

Resumé

Formal analysis of timing constraints is crucial
in safety-critical cyber-physical systems (CPS). EAST-ADL is
an architectural language dedicated to safety-critical embedded
system design. SIMULINK/STATEFLOW (S/S) is an industrial tool
widely used for modeling and analysis of CPS. In most cases, a
bounded number of violations of timing constraints in CPS would
not lead to system failures when the results of the violations are
negligible, called Weakly-Hard (WH). In the context of WH,
this paper presents an SMT-based approach to support formal
probabilistic analysis of timing constraints in CPS modeled in
EAST-ADL and S/S. Our approach is demonstrated on two
automotive systems case studies.
OriginalsprogEngelsk
Publikationsdatookt. 2018
StatusUdgivet - okt. 2018
BegivenhedFormal Methods in Computer-Aided Design - Austin, USA
Varighed: 30. okt. 20182. nov. 2018

Konference

KonferenceFormal Methods in Computer-Aided Design
LandUSA
ByAustin
Periode30/10/201802/11/2018

Fingeraftryk

Surface mount technology
Cyber Physical System

Citer dette

Kang, E-Y., & Huang, L. (2018). SMT-based Probabilistic Analysis of Timing Constraints in Cyber-Physical Systems. Poster session præsenteret på Formal Methods in Computer-Aided Design, Austin, USA.
Kang, Eun-Young ; Huang, Li. / SMT-based Probabilistic Analysis of Timing Constraints in Cyber-Physical Systems. Poster session præsenteret på Formal Methods in Computer-Aided Design, Austin, USA.
@conference{366f927b48424c1394a304d472510eb9,
title = "SMT-based Probabilistic Analysis of Timing Constraints in Cyber-Physical Systems",
abstract = "Formal analysis of timing constraints is crucialin safety-critical cyber-physical systems (CPS). EAST-ADL isan architectural language dedicated to safety-critical embeddedsystem design. SIMULINK/STATEFLOW (S/S) is an industrial toolwidely used for modeling and analysis of CPS. In most cases, abounded number of violations of timing constraints in CPS wouldnot lead to system failures when the results of the violations arenegligible, called Weakly-Hard (WH). In the context of WH,this paper presents an SMT-based approach to support formalprobabilistic analysis of timing constraints in CPS modeled inEAST-ADL and S/S. Our approach is demonstrated on twoautomotive systems case studies.",
author = "Eun-Young Kang and Li Huang",
year = "2018",
month = "10",
language = "English",
note = "null ; Conference date: 30-10-2018 Through 02-11-2018",

}

Kang, E-Y & Huang, L 2018, 'SMT-based Probabilistic Analysis of Timing Constraints in Cyber-Physical Systems' Formal Methods in Computer-Aided Design, Austin, USA, 30/10/2018 - 02/11/2018, .

SMT-based Probabilistic Analysis of Timing Constraints in Cyber-Physical Systems. / Kang, Eun-Young; Huang, Li.

2018. Poster session præsenteret på Formal Methods in Computer-Aided Design, Austin, USA.

Publikation: Konferencebidrag uden forlag/tidsskriftPosterForskningpeer review

TY - CONF

T1 - SMT-based Probabilistic Analysis of Timing Constraints in Cyber-Physical Systems

AU - Kang, Eun-Young

AU - Huang, Li

PY - 2018/10

Y1 - 2018/10

N2 - Formal analysis of timing constraints is crucialin safety-critical cyber-physical systems (CPS). EAST-ADL isan architectural language dedicated to safety-critical embeddedsystem design. SIMULINK/STATEFLOW (S/S) is an industrial toolwidely used for modeling and analysis of CPS. In most cases, abounded number of violations of timing constraints in CPS wouldnot lead to system failures when the results of the violations arenegligible, called Weakly-Hard (WH). In the context of WH,this paper presents an SMT-based approach to support formalprobabilistic analysis of timing constraints in CPS modeled inEAST-ADL and S/S. Our approach is demonstrated on twoautomotive systems case studies.

AB - Formal analysis of timing constraints is crucialin safety-critical cyber-physical systems (CPS). EAST-ADL isan architectural language dedicated to safety-critical embeddedsystem design. SIMULINK/STATEFLOW (S/S) is an industrial toolwidely used for modeling and analysis of CPS. In most cases, abounded number of violations of timing constraints in CPS wouldnot lead to system failures when the results of the violations arenegligible, called Weakly-Hard (WH). In the context of WH,this paper presents an SMT-based approach to support formalprobabilistic analysis of timing constraints in CPS modeled inEAST-ADL and S/S. Our approach is demonstrated on twoautomotive systems case studies.

M3 - Poster

ER -

Kang E-Y, Huang L. SMT-based Probabilistic Analysis of Timing Constraints in Cyber-Physical Systems. 2018. Poster session præsenteret på Formal Methods in Computer-Aided Design, Austin, USA.