NDLI: Formal Analysis of Robustness at Model and Code Level

Please wait, while we are loading the content...

A Decision Tree Approach to Data Classification using Signal Temporal Logic

Computing the Domain of Attraction of Switching Systems Subject to Non-Convex Constraints

Case Studies in Data-Driven Verification of Dynamical Systems

Safety Analysis of Automotive Control Systems Using Multi-Modal Port-Hamiltonian Systems

Symbolic-Numeric Reachability Analysis of Closed-Loop Control Software

Adaptive Decentralized MAC for Event-Triggered Networked Control Systems

Control Synthesis for Large Collections of Systems with Mode-Counting Constraints

Optimal Co-Design of Scheduling and Control for Networked Systems

Entropy and Minimal Data Rates for State Estimation and Model Detection

Computing Distances between Reach Flowpipes

Temporal Logic as Filtering

Generating Unstable Trajectories for Switched Systems via Dual Sum-Of-Squares Techniques

Towards Model Checking of Implantable Cardioverter Defibrillators

Verification and Synthesis of Timing Contracts for Embedded Controllers

SMT-Based Analysis of Virtually Synchronous Distributed Hybrid Systems

Event-Separation Properties and Asymptotic Behaviour of Hybrid Event-Based Control Systems

Compositional Synthesis with Parametric Reactive Controllers

Safety Verification of Piecewise-Deterministic Markov Processes

Reachset Conformance Testing of Hybrid Automata

Directed Specifications and Assumption Mining for Monotone Dynamical Systems

A Topological Method for Finding Invariant Sets of Switched Systems

SL2SX Translator: From Simulink to SpaceEx Models

Formal Analysis of Robustness at Model and Code Level

Scalable Static Hybridization Methods for Analysis of Nonlinear Systems

Semi-autonomous Intersection Collision Avoidance through Job-shop Scheduling

Nonlinear Controller Synthesis and Automatic Workspace Partitioning for Reactive High-Level Behaviors

From Simulation Models to Hybrid Automata Using Urgency and Relaxation

Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications

Hybridization for Stability Analysis of Switched Linear Systems

SCOTS: A Tool for the Synthesis of Symbolic Controllers

Building Power Consumption Models from Executable Timed I/O Automata Specifications

Robust Asymptotic Stabilization of Hybrid Systems using Control Lyapunov Functions

Parallelotope Bundles for Polynomial Reachability

Formal Analysis of Robustness at Model and Code Level

Content Provider	ACM Digital Library
Author	Roux, Pierre Jobredeaux, Romain Garoche, Pierre-Loïc Wang, Timothy E. Féron, Éric
Abstract	Robustness analyses play a major role in the synthesis and analysis of controllers. For control systems, robustness is a measure of the maximum tolerable model inaccuracies or perturbations that do not destabilize the system. Analyzing the robustness of a closed-loop system can be performed with multiple approaches: gain and phase margin computation for single-input single-output (SISO) linear systems, mu analysis, IQC computations, etc. However, none of these techniques consider the actual code in their analyses. The approach presented here relies on an invariant computation on the discrete system dynamics. Using semi-definite programming (SDP) solvers, a Lyapunov-based function is synthesized that captures the vector margins of the closed-loop linear system considered. This numerical invariant expressed over the state variables of the system is compatible with code analysis and enables its validation on the code artifact. This automatic analysis extends verification techniques focused on controller implementation, addressing validation of robustness at model and code level. It has been implemented in a tool analyzing discrete SISO systems and generating over-approximations of phase and gain margins. The analysis will be integrated in our toolchain for Simulink and Lustre models autocoding and formal analysis.
Starting Page	125
Ending Page	134
Page Count	10
File Format	PDF
ISBN	9781450339551
DOI	10.1145/2883817.2883824
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2016-04-11
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Control software Static analysis Robustness margins Semi-definite programming Formal verification
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Formal software verification at model and at source code levels (2013).

Formal verification of software source code through semi-automatic modeling (2005)

Proving Temporal Properties at Code Level for Basic Operators of Control/Command Programs

Formal verification of software source code through semi-automatic modeling (2005)

Formal verification, engineering and business value.

Static Code Analysis for Software Security Verification: Problems and Approaches

Generating runtime verification specifications based on static code analysis alerts

A Survey of Automated Techniques for Formal Software Verification (2008)

Eliminating Dead-Code from XQuery Programs (2010)

Formal Analysis of Robustness at Model and Code Level

Similar Documents

Formal software verification at model and at source code levels (2013).

Formal verification of software source code through semi-automatic modeling (2005)

Proving Temporal Properties at Code Level for Basic Operators of Control/Command Programs

Formal verification of software source code through semi-automatic modeling (2005)

Formal verification, engineering and business value.

Static Code Analysis for Software Security Verification: Problems and Approaches

Generating runtime verification specifications based on static code analysis alerts

A Survey of Automated Techniques for Formal Software Verification (2008)

Eliminating Dead-Code from XQuery Programs (2010)

Formal Analysis of Robustness at Model and Code Level