Start Submission Become a Reviewer

Reading: Integrating runtime validation and hardware-in-the-loop (HiL) testing with V & V in complex ...

Download

A- A+
Alt. Display

Research Articles

Integrating runtime validation and hardware-in-the-loop (HiL) testing with V & V in complex hybrid systems

Authors:

S.D. Dewasurendra ,

University of Peradeniya, LK
About S.D.
Department of Computer Engineering, Faculty of Engineering
X close

A.C. Vidanapathirana,

Industrial Service Bureau (ISB), Kurunegala, LK
X close

S.G. Abeyratne

University of Peradeniya, LK
About S.G.
Department of Electrical and Electronic Engineering, Faculty of Engineering,
X close

Abstract

 This study addresses the problem of assuring provably safe and correct behaviour of safety-critical complex hybrid systems (CHS) throughout their life-cycles when physical system dynamics tend to change due to natural causes. Model-based development methods are needed that integrate formal specification, verification, implementation level testing and runtime validation. Scalability limitations of available algorithms/methods dictate a modular approach, but this poses conflicting issues of compositionality, falsetransitivity, soundness and completeness. In this paper a compositional solution approach based on the decomposition and hybridisation of statechart models (into hybrid automata - HA) is demonstrated. Specifically, a compositional formal verification methodology developed earlier for discrete event dynamic systems (DEDS) was elevated to hybrid dynamics, successfully overcoming the risk of false transitivity common to direct abstraction methods of continuous state-space. It was then used to develop a scalable strategy to generate sound and complete (relative to coverage criteria) tests, and configure corresponding compositional HiL tests for different abstraction and functional levels. The same decomposition was used to derive compositional runtime validation tests based on discrete invariants and differential invariants. The study formally proves that (1) the proposed HA based formal verification method is compositional, sound and complete relative to first-order logic of differential equations, (2) the modular tests are compositional and (3) the HA based test generation method is compositional, sound and complete relative to first-order logic of differential equations. To reduce complexity compositionality is rendered parallel than sequential to perform the simpler tasks concurrently. The claims have been validated experimentally on a full scale experimental rig.

How to Cite: Dewasurendra, S.D., Vidanapathirana, A.C. and Abeyratne, S.G., 2020. Integrating runtime validation and hardware-in-the-loop (HiL) testing with V & V in complex hybrid systems. Journal of the National Science Foundation of Sri Lanka, 47(4), pp.393–408. DOI: http://doi.org/10.4038/jnsfsr.v47i4.9678
Published on 25 Jan 2020.
Peer Reviewed

Downloads

  • PDF (EN)

    comments powered by Disqus