English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

The presence of a tight integration between the discrete control (the"cyber") and the analog environment (the "physical")---via sensors andactuators over wired or wireless communication networks---is the definingfeature of cyber-physical systems. Hence, the functional correctness of acyber- physical system is crucially dependent not only on the dynamics of theanalog physical environment, but also on the decisions taken by the discretecontrol that alter the dynamics of the environment. The framework of Hybridautomata---introduced by Alur, Courcoubetis, Henzinger, and Ho---provides aformal modeling and specification environment to analyze the interactionbetween the discrete and continuous parts of a cyber-physical system. Hybridautomata can be considered as generalizations of finite state automataaugmented with a finite set of real-valued variables whose dynamics in eachstate is governed by a system of ordinary differential equations. Moreover, thediscrete transitions of hybrid automata are guarded by constraints over thevalues of these real-valued variables, and enable discontinuous jumps in theevolution of these variables. Considering the richness of the dynamics in ahybrid automaton, it is perhaps not surprising that the fundamentalverification questions, like reachability and schedulability, for the generalmodel are undecidable. In this article we present a review of hybrid automataas modeling and verification framework for cyber-physical systems, and surveysome of the key results related to practical verification questions related tohybrid automata.

Hybrid Automata for Formal Modeling and Verification of Cyber-Physical Systems