Combining test case generation and runtime verification

DOI10.1016/J.TCS.2004.11.007MaRDI QIDQ555778zbMATH OpenOpenAlexFDO

Authors Jianyong Qiao, Sumit K. Garg

Publication date 10 June 2005

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2004.11.007

zbMATH Keywords

Automated testingConcurrency analysisModel checkingNASA rover controllerRuntime verificationSymbolic executionTemporal logicTest case generation

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1951185
• Towards a framework for constraint-based test case generation
• scientific article; zbMATH DE number 2079824
• Formal Approaches to Software Testing
• Model checking, testing and verification working together

Cites work

• scientific article; zbMATH DE number 1670567 (Why is no real title available?)
• scientific article; zbMATH DE number 3502759 (Why is no real title available?)
• scientific article; zbMATH DE number 1956607 (Why is no real title available?)
• scientific article; zbMATH DE number 2080058 (Why is no real title available?)
• scientific article; zbMATH DE number 2087636 (Why is no real title available?)
• A suite of tools for debugging distributed autonomous systems
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• An overview of the runtime verification tool Java PathExplorer
• Checking finite traces using alternating automata
• Computer Aided Verification
• Evolving Algebras 1993: Lipari Guide
• Experimental evaluation of verification and validation tools on Martian Rover software
• Java-MaC: A run-time assurance approach for Java programs
• MetateM: An introduction
• Model checking a path (preliminary report)
• Symbolic execution and program testing
• Verification, Model Checking, and Abstract Interpretation

Cited in

(12)

• Automation of broad sanity test generation
• Computer says no: verdict explainability for runtime monitors using a local proof system
• On runtime enforcement via suppressions
• Weak Kripke structures and LTL
• Automatic generation of test oracles -- from pilot studies to application
• scientific article; zbMATH DE number 1951185 (Why is no real title available?)
• Integration of verification methods for program systems
• On first-order runtime enforcement of branching-time properties
• Mu-calculus path checking
• Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
• Construction and analysis of ground models and their refinements as a foundation for validating computer-based systems
• Theoretical Aspects of Computing - ICTAC 2004

Describes a project that uses

Uses Software

• TGV
• AGEDIS
• JNuke
• AsmL
• pthreads
• JPAX
• QuickCheck
• Korat
• TestEra

This page was built for publication: Combining test case generation and runtime verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q555778)