+

Ranville, 2004 - Google Patents

Case Study of Commercially Available Tools that Apply Formal Methods to a Matlab/Simulink/Stateflow Model

Ranville, 2004

Document ID
16326288715745494192
Author
Ranville S
Publication year

External Links

Snippet

This paper will apply a number of commercially available formal methods tools to discrete Matlab models and will report these results. After introducing formal methods, the features and ease of use of each tool will be reported as well as describing how this will benefit the …
Continue reading at www.sae.org (other versions)

Classifications

    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/3668—Software testing
    • G06F11/3672—Test management
    • G06F11/3688—Test management for test execution, e.g. scheduling of test suites
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5009—Computer-aided design using simulation
    • G06F17/504—Formal methods
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/3668—Software testing
    • G06F11/3696—Methods or tools to render software testable
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5009—Computer-aided design using simulation
    • G06F17/5022—Logic simulation, e.g. for logic circuit operation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/22—Detection or location of defective computer hardware by testing during standby operation or during idle time, e.g. start-up testing
    • G06F11/26—Functional testing
    • G06F11/263—Generation of test inputs, e.g. test vectors, patterns or sequences; with adaptation of the tested hardware for testability with external testers
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/3664—Environments for testing or debugging software
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/3604—Software analysis for verifying properties of programs
    • G06F11/3608—Software analysis for verifying properties of programs using formal methods, e.g. model checking, abstract interpretation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/362—Software debugging
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/22—Detection or location of defective computer hardware by testing during standby operation or during idle time, e.g. start-up testing
    • G06F11/2205—Detection or location of defective computer hardware by testing during standby operation or during idle time, e.g. start-up testing using arrangements specific to the hardware being tested
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F2217/00—Indexing scheme relating to computer aided design [CAD]
    • G06F2217/86—Hardware-Software co-design
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G—PHYSICS
    • G01—MEASURING; TESTING
    • G01R—MEASURING ELECTRIC VARIABLES; MEASURING MAGNETIC VARIABLES
    • G01R31/00—Arrangements for testing electric properties; Arrangements for locating electric faults; Arrangements for electrical testing characterised by what is being tested not provided for elsewhere
    • G01R31/28—Testing of electronic circuits, e.g. by signal tracer
    • G01R31/317—Testing of digital circuits
    • G01R31/3181—Functional testing
    • G01R31/3183—Generation of test inputs, e.g. test vectors, patterns or sequence
    • G01R31/318342—Generation of test inputs, e.g. test vectors, patterns or sequence by preliminary fault modelling, e.g. analysis, simulation
    • G—PHYSICS
    • G05—CONTROLLING; REGULATING
    • G05B—CONTROL OR REGULATING SYSTEMS IN GENERAL; FUNCTIONAL ELEMENTS OF SUCH SYSTEMS; MONITORING OR TESTING ARRANGEMENTS FOR SUCH SYSTEMS OR ELEMENTS
    • G05B23/00—Testing or monitoring of control systems or parts thereof
    • G05B23/02—Electric testing or monitoring
    • G05B23/0205—Electric testing or monitoring by means of a monitoring system capable of detecting and responding to faults
    • G05B23/0218—Electric testing or monitoring by means of a monitoring system capable of detecting and responding to faults characterised by the fault detection method dealing with either existing or incipient faults
    • G05B23/0256—Electric testing or monitoring by means of a monitoring system capable of detecting and responding to faults characterised by the fault detection method dealing with either existing or incipient faults injecting test signals and analyzing monitored process response, e.g. injecting the test signal while interrupting the normal operation of the monitored system; superimposing the test signal onto a control signal during normal operation of the monitored system

Similar Documents

Publication Publication Date Title
Bochot et al. Model checking flight control systems: The Airbus experience
US8751094B2 (en) Method for validation of a graphically based executable control specification using model extraction
Murphy et al. Best practices for verification, validation, and test in model-based design
Ranville Case study of commercially available tools that apply formal methods to a Matlab/Simulink/Stateflow model
Elmqvist et al. Safety-oriented design of component assemblies using safety interfaces
Win et al. Using simulated execution in verifying distributed algorithms
Dragomir et al. Model-checking of space systems designed with TASTE/SDL
Erkkinen et al. Verification, validation, and test with model-based design
Zafar et al. Towards a workflow for model-based testing of embedded systems
Fummi et al. On the use of a high-level fault model to check properties incompleteness
Canny et al. An approachable and partially automated specification modeling workflow
Yang et al. An effective model-based development process using simulink/stateflow for automotive body control electronics
Ackermann et al. Model based design verification: A monitor based approach
Semenov Automation of Hardware-in-the-Loop and In-the-Vehicle testing and validation for Hybrid Electric Vehicles at Ford
Desel et al. Model validation in controller design
Erkkinen Production code generation for safety-critical systems
Böde et al. Adding value to automotive models
Erkkinen Model style guidelines for production code generation
Stone et al. Improved modeling and validation of command sequences using a checkable sequence language
Achrifi Coverage verification framework for ADAS models
Banerjee et al. Can Semi-Formal be Made More Formal?
Dadfarnia et al. Platform-Independent Debugging of Physical Interaction and Signal Flow Models
Stumptner et al. A model-based tool for finding faults in hardware designs
Heitmeyer et al. Computing the Next-State Function of a Requirements Model
Naydich et al. Flight guidance system validation using Spin
点击 这是indexloc提供的php浏览器服务，不要输入任何密码和下载