China
Africa
Explore chapters and articles related to this topic
Software Development Methods and Tools
Published in Paul H. King, Richard C. Fries, Arthur T. Johnson, Design of Biomedical Devices and Systems, 2018
Paul H. King, Richard C. Fries, Arthur T. Johnson
Some of the implementation techniques of formal static analysis include the following: Model checking considers systems that have finite state or may be reduced to finite state by abstractionData flow analysis is a lattice-based technique for gathering information about the possible set of valuesAbstract interpretation models the effect that every statement has on the state of an abstract machine (i.e., it “executes” the software based on the mathematical properties of each statement and declaration). This abstract machine over-approximates the behaviors of the system: the abstract system is thus made simpler to analyze, at the expense of incompleteness (not every property true of the original system is true of the abstract system). If properly done, though, abstract interpretation is sound (every property true of the abstract system can be mapped to a true property of the original system). The Frama-c framework and Polyspace heavily rely on abstract interpretation.Use of assertions in program code as first suggested by Hoare logic. There is tool support for some programming languages (e.g., the SPARK programming language (a subset of Ada) and the Java Modeling Language (JML) using ESC/Java and ESC/Java2, ANSI/ISO C Specification Language for the C language).
Mathworks Approach to MBD
Published in Cary R. Spitzer, Uma Ferrell, Thomas Ferrell, Digital Avionics Handbook, 2017
Bill Potter, Pieter Mosterman, Tom Erkkinen
Simulink Code Inspector [5] is a separate tool that can be used to verify C source code developed from Embedded Coder. This tool interrogates the model using the Simulink API to read data from the model. The model is converted into a different intermediate representation, in the form of an abstract syntax tree, for use in the code inspection process. The Simulink Code Inspector also uses the generated C code files as input and parses these into a different intermediate representation that can be compared to the model’s intermediate representation. The tool outputs an inspection report and a traceability report for the source code. Polyspace is a tool that has two capabilities: coding standards checking (e.g., MISRA AC AGC [6]) and run-time error detection. The main input to Polyspace is the source code; however, it can optionally read range specification data from the model using the Simulink API. When using the Polyspace Model Link SL product, it can trace defects found in the source code back to the source blocks in the model. Polyspace also supports any C code, whether it is automatically generated or manually developed. For run-time error detection, Polyspace uses abstract interpretation in its formal methods engine.
A GCC-based checker for compliance with MISRA-C's single-translation-unit rules
Published in Connection Science, 2023
Chih-Yuan Chen, Yung-An Fang, Guan-Ren Wang, Peng-Sheng Chen
Several static analysis tools can detect whether a program is compliant with the MISRA-C rules. These tools are either commercial or open source. Examples of commercial software include Parasoft (Parasoft, n.d.), PC-Lint (Vector Informatik, n.d.), Helix QAC (Perforce Software, n.d.), PVS-Studio (PVS-Studio, n.d.), IAR C-STAT (IAR Systems, n.d.), Coverity (Synopsys, n.d.a), CodeSonar (GrammaTech, n.d.), and Polyspace (MathWorks, n.d.). The most well-known and widely used open-source tool is Cppcheck (Cppcheck, n.d.), which can detect software bugs, undefined behavior, dangerous coding constructs, and coding style. In Cppcheck, a program is preprocessed to an internal token list. Each token can access the related syntax tree and symbol information via proper APIs. The checker analyzes the token list according to pre-defined rules. Cppcheck also contains a value-flow analysis and simple control-flow analysis to improve the correctness of the analysis. Users can easily customise checking rules to meet their needs. All these tools are third-party software independent of the compiler.