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 Plus annual

Presents the access of premium content as premium feature

Premium Content

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 Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

This paper examines the verification of stability, a control requirement,over discrete control systems represented as Simulink diagrams, using differentmodel checking approaches and tools. Model checking comprises the (exhaustive)exploration of a model of a system, to determine if a requirement is satisfied.If that is not the case, examples of the requirement's violation within thesystem's model are provided, as witnesses. These examples are potentiallycomplementary to previous work on automatic theorem proving, when a system isnot proven to be stable, but no proof of instability can be provided.  We experimentally evaluated the suitability of four model checking approachesto verify stability on a set of benchmarks including linear and nonlinear,controlled and uncontrolled, discrete systems, via Lyapunov's second method orLyapunov's direct method. Our study included symbolic, bounded, statistical andhybrid model checking, through the open-source tools NuSMV, UCLID, S-TaLiRo andSpaceEx, respectively. Our experiments and results provide an insight on thestrengths and limitations of these model checking approaches for theverification of control requirements for discrete systems at Simulink level. Wefound that statistical model checking with S-TaLiRo is the most suitable optionto complement our previous work on automatic theorem proving.

Evaluating Model Checking Approaches to Verify Stability of Control Systems in Simulink