Testing Based Techniques for Verification and Validation of Cyber-Physical Systems

diagram for Testing Based Techniques for Verification and Validation of Cyber-Physical Systems

Principal Investigator

Parasara Sridhar Duggirala

Computer Science and Engineering, UConn

Graduate Fellows

Abolfazal Karimi

Project Duration

1 Year

Project Summary

This project is aimed at developing an automated testing framework for verification and validation of Cyber-Physical Systems. Given that an industrial scale CPS has many components and each component is designed by many engineers, the verification and validation process for a CPS becomes a very challenging task. Our central hypothesis is to perform systematic testing of Cyber-Physical Systems, obtain the test results, and apply a classification technique over these observed behaviors to infer patterns among executions. The patterns obtained after applying the classification techniques would reveal intuition behind the tests and specifications and reflect the requirements that are imposed on the system.

 As a part of this project, new learning methods on behaviors of the continuous systems were developed. Primarily, the discrepancy between tests and the underlying dimensionality of the test vectors were understood by formulating optimization problems and principle component analysis. This
dimensionality and discrepancy were used for generating a
variety of executions that violate a specific safety requirement
called as longest and deepest counterexample.

Program Applications

-Initial: Models of powertrain control systems from Toyota MBD group.

-Interim: Model of chiller plants developed by Prof. Bollas.

-Final: Commercial models of CCS.

Project Outputs

-1 PhD student being trained.

-5 collaborators from UTC business units.

-2 scientific publications.

-2 software artifacts.

1 UTC fellowship.

Business Unit Benefit

-Generating automatic test vectors for compositional and hierarchical Cyber-Physical Systems.

-Automatically inferring whether the specification is satisfied by the model.

-Obtaining counterexamples for behaviors that violate the specification.

 

Benefits to the UTC-IASE

-External funding from NSF awarded to the PI that leverages the techniques of this proposal.

Talent Creation

-1 PhD student working on this UTAS project.

Excellence Artifacts

-2 scientific papers.

-2 software artifacts.

 

Curriculum Enhancement

SE 5301, SE 5302

Business Unit Engagement

-1 collaborator from UTAS, 1 from UTAS Ireland, 3 from UTRC Italy.
40 hrs (1 yr) of UTC engagement.

Example Publications and Further Reading

-Manish Goyal, Parasara Sridhar Duggirala. On Generation of a Variety of Counterexamples for Linear Hybrid Systems (Currently under review), 2018.

-Manish Goyal, Parasara Sridhar Duggirala. LADDER: A tool for learning discrepancy functions and dimensionality of trajectories. (Under preparation). 2018.

-Parasara Sridhar Duggirala, Mahesh Viswanathan. Parsimonious, Simulation Based Verification of Linear Systems. International Conference on Computer Aided Verification (CAV) 2016.

High dimensionality, complex design, and nonlinearity are typical characteristic properties of industrial scale Cyber-Physical Systems. An execution of such CPS would involve mix of continuous and discrete behaviors where the continuous behaviors correspond to the evolution of the physical parameters (or systems variables) over time and discrete transitions correspond to the changes in the software state. The requirements for these systems (given in a natural language) describe the behavior of the system using the predicates on software state and the physical state. For example, a requirement of HVAC system can be specified as “the ambient air temperate should reduce by at least 5 units within 10 minutes of activating the high mode." Given several such requirements, validation is the process of inferring whether a given requirement is valid. Given a valid requirement, verification is the process of inferring whether all the behaviors of the system satisfy the given requirement. In this proposal, we outline dynamic analysis techniques for validation and verification of CPS. Our central hypothesis in this proposal is to perform systematic testing of Cyber-Physical Systems, obtain the test results, and apply a classification technique over these observed behaviors to infer patterns among executions. These patters would reflect the requirements that are imposed on the system. The focus of this project would be to tackle the underlying set of requirements and the techniques that are useful in classification.

Relevant Publications

Peer Reviewed Papers

  1. P. S. Duggirala, S. Mitra, M. Viswanathan, “Verification of Annotated Models From Executions” International Conference on Embedded Software (EMSOFT) October 2013.
  2. P. S. Duggirala, L. Wang, S. Mitra, M. Viswanathan, C. Munoz “Temporal Precedence Checking for Switched Models and its Application to a Parallel Landing Protocol” International Symposium on Formal Methods (FM) May 2014.
  3. P. S. Duggirala, S. Mitra, M. Viswanathan, M. Potok, “C2E2:  A Verification Tool for Stateflow Models” Tools and Algorithms for the Construction and Analysis of Systems (TACAS) April 2015.
  4. P. S. Duggirala, C. Fan, S. Mitra, M. Viswanathan, “Meeting a Powertrain Verification Challenge” International Conference on Computer Aided Verification (CAV) July 2015.
  5. P. S. Duggirala, M. Viswanathan, “Parsimonious, Simulation Based Verification of Linear Systems” International Conference on Computer Aided Verification (CAV) July 2016.
  6. C. Fan, B. Qi, S. Mitra, M. Viswanathan, P. S. Duggirala, “Automatic Reachability Analysis  for  Nonlinear  Hybrid  Models  With  C2E2” International  Conference  on  Computer  Aided Verification (CAV) July 2016.
  7. S. Bak, P. S. Duggirala, “HyLAA: A Tool for Computing Simulation-Equivalent Reachability for Linear Systems” International Conference on Hybrid Systems Computation and Control (HSCC) April 2017.
  8. S. Bak, P. S. Duggirala, “Rigorous Simulation Based Analysis of Linear Hybrid Systems” Tools and Algorithms for the Construction and Analysis of Systems (TACAS) April 2017.