Formal Requirement Debugging for Testing and Verification of Cyber-Physical Systems

No abstract is available for this paper.

• Publication year

  2016

• Venue

  ACM Transactions on Embedded Computing Systems

• Publication date

  2016-07-08

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.1145/3147451
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Model Checking

  2018influential reference
• Vacuity aware falsification for MTL request-response specifications

  2017cited by this paper
• Simulation-guided approaches for verification of automotive powertrain control systems

  2015influential reference
• VISPEC: A graphical tool for elicitation of MTL requirements

  2015influential reference
• Vacuity in practice: temporal antecedent failure

  2015cited by this paper
• Metric interval temporal logic specification elicitation and debugging

  2015influential reference
• A Logical Characterization of Timed (non-)Regular Languages

  2014cited by this paper
• Low-Effort Specification Debugging and Analysis

  2014cited by this paper
• Benchmarks for Temporal Logic Requirements for Automotive Systems

  2014influential reference
• Optimal strategy synthesis for request-response games

  2014cited by this paper
• Towards Formal Specification Visualization for Testing and Monitoring of Cyber-Physical Systems

  2014influential reference
• Deciding the Satisfiability of MITL Specifications

  2013influential reference
• LTL Satisfiability Checking Revisited

  2013cited by this paper
• Probabilistic Temporal Logic Falsification of Cyber-Physical Systems

  2013influential reference
• Mining Requirements From Closed-Loop Control Models

  2013influential reference
• A tool for deciding the satisfiability of continuous-time metric temporal logic

  2013influential reference
• Querying Parametric Temporal Logic Properties on Embedded Systems

  2012cited by this paper
• On the revision problem of specification automata

  2012cited by this paper
• Verification of automotive control applications using S-TaLiRo

  2012influential reference
• Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies

  2011cited by this paper
• S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems

  2011influential reference
• Vacuous real-time requirements

  2011cited by this paper
• Analyzing Unsynthesizable Specifications for High-Level Robot Behavior Using LTLMoP

  2011cited by this paper
• Revising temporal logic specifications for motion planning

  2011cited by this paper
• Timed Property Sequence Chart

  2010influential reference
• Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems

  2010influential reference
• Before and after vacuity

  2009influential reference
• A Framework for Inherent Vacuity

  2009influential reference
• Vacuity in Testing

  2008influential reference
• Diagnostic Information for Realizability

  2008cited by this paper
• A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance

  2008cited by this paper
• Graphical scenarios for specifying temporal properties: an automated approach

  2007influential reference
• Temporal Antecedent Failure: Refining Vacuity

  2007influential reference
• LTL satisfiability checking

  2007cited by this paper
• Managing space for finite-state verification

  2006influential reference
• Efficient monitoring of safety properties

  2004influential reference
• Monitoring Algorithms for Metric Temporal Logic Specifications

  2004cited by this paper
• Monitoring Temporal Properties of Continuous Signals

  2004influential reference
• Enhanced Vacuity Detection in Linear Temporal Logic

  2003cited by this paper
• Debugging temporal specifications with concept analysis

  2003cited by this paper
• An automata-theoretic approach to constraint LTL

  2002influential reference
• Efficient Detection of Vacuity in Temporal Model Checking

  2001influential reference
• Vacuity detection in temporal model checking

  1999influential reference
• Property specification patterns for finite-state verification

  1998influential reference
• The Algorithmic Analysis of Hybrid Systems

  1995influential reference
• Formally Verifying a Microprocessor Using a Simulation Methodology

  1994cited by this paper
• The benefits of relaxing punctuality

  1991influential reference
• Specifying real-time properties with metric temporal logic

  1990cited by this paper
• Formal Aspects of Computing Formal Aspects of Computing Model checking Duration Calculus: a practical approach ∗

  year unknowncited by this paper

• MightyPPL: Verification of MITL with Past and Pnueli Modalities

  2025cites this paper
• A Tree-Shaped Tableau for Checking the Satisfiability of Signal Temporal Logic with Bounded Temporal Operators

  2025influential citation
• THE SECURITY REQUIREMENTS FOR CYBER-PHYSICAL SYSTEMS

  2024cites this paper
• A Usage-Aware Sequent Calculus for Differential Dynamic Logic

  2023cites this paper
• Formalizing and evaluating requirements of perception systems for automated vehicles using spatio-temporal perception logic

  2022cites this paper
• Adopting formal methods on requirements verification and validation for cyber-physical systems: A systematic literature review

  2022cites this paper
• PyFoReL: A Domain-Specific Language for Formal Requirements in Temporal Logic

  2022cites this paper
• Adaptive testing for specification coverage and refinement in CPS models

  2022cites this paper
• Mutated Specification-Based Test Data Generation with a Genetic Algorithm

  2021cites this paper
• A Study on Challenges of Testing Robotic Systems

  2020cites this paper
• Extending Signal Temporal Logic with Quantitative Semantics by Intervals for Robust Monitoring of Cyber-physical Systems

  2020cites this paper
• TLTk: A Toolbox for Parallel Robustness Computation of Temporal Logic Specifications

  2020cites this paper
• Runtime Verification: 20th International Conference, RV 2020, Los Angeles, CA, USA, October 6–9, 2020, Proceedings

  2020cites this paper
• Unified Devs-Based Platform for Modeling and Simulation of Hybrid Control Systems

  2020cites this paper
• Specification-guided Software Fault Localization for Autonomous Mobile Systems

  2020cites this paper
• Property specification patterns at work: verification and inconsistency explanation

  2019cites this paper
• Falsification of Signal-Based Specifications for Cyber-Physical Systems

  2019cites this paper
• Search-based Test Generation for Automated Driving Systems: From Perception to Control Logic

  2019cites this paper
• Enhancing Temporal Logic Falsification With Specification Transformation and Valued Booleans

  2019cites this paper
• Robustness of Specifications and Its Applications to Falsification, Parameter Mining, and Runtime Monitoring with S-TaLiRo

  2019cites this paper
• Software requirements testing approaches: a systematic literature review

  2019cites this paper
• Cyber-Physical Systems, a new formal paradigm to model redundancy and resiliency

  2018cites this paper
• Temporal Logic (TL)-Based Autonomy for Smart Manufacturing Systems

  2018cites this paper
• Optimal Multi-Valued LTL Planning for Systems with Access Right Levels

  2018cites this paper
• Timed-Automata-Based Verification of MITL over Signals

  2017cites this paper
• MightyL: A Compositional Translation from MITL to Timed Automata

  2017influential citation
• Consistency of Property Specification Patterns with Boolean and Constrained Numerical Signals

  2017cites this paper