SPHIN: A model checker for reconfigurable hybrid systems based on SPIN | Zendy

Hosung Song | Zendy; Kevin J. Compton | Zendy; William C. Rounds | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

SPHIN: A model checker for reconfigurable hybrid systems based on SPIN

Author(s) -

Hosung Song,

Kevin J. Compton,

William C. Rounds

Publication year - 2006

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2005.10.011

Subject(s) - promela , computer science , model checking , syntax , programming language , semantics (computer science) , channel (broadcasting) , hybrid system , theoretical computer science , spin (aerodynamics) , artificial intelligence , physics , computer network , machine learning , thermodynamics

We present SPHIN, a model checker for reconfigurable hybrid systems based on the model checker SPIN. We observe that physical (analog) mobility can be modeled in the same way as logical (discrete) mobility is modeled in the π-calculus by means of channel name passing. We chose SPIN because it supports channel name passing and can model reconfigurations. We extend the syntax of PROMELA and the verification algorithms based on the expected semantics. We demonstrate the tool's capabilities by modeling and verifying a reconfigurable hybrid system

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research