English
Using formal methods for sophisticated static code analysis
Jay Abraham, MathWorks
EETimes (6/6/2012 2:21 PM EDT)
In this Product How-To design article, Jay Abraham of Mathworks uses the company’s Polyspace code verifier to explain the use formal methods-based static code analysis to ensure high quality and verifiable embedded software.
Software underlies applications in a multitude of industries today. Aircraft, automobiles, industrial machinery, and medical devices all contain specialized software known as embedded software. This software is directly responsible for a variety of critical tasks. This software must be of high quality and must be thoroughly tested to verify it performs as expected.
In such critical systems, even simple operations performed with software can be fraught with risk. For example, consider an algorithm that requires the addition operation. If the underlying 32-bit microcontroller does not have a floating point unit, you need to be careful to avoid overflow conditions.
|
E-mail This Article | 
|
|
Printer-Friendly Page |
Related Articles
- Five steps to reliable, low-cost, bug-free software with static code analysis
- Think static analysis cures all ills? Think again.
- Formal property verification: A tale of two methods
- Using static analysis to detect coding errors in open source security-critical server applications
- Static timing analysis: bridging the gap between simulation and silicon
New Articles
- Understanding MACsec and Its Integration
- Discover new Tessent UltraSight-V from Siemens EDA, and accelerate your RISC-V development.
- The Critical Factors of a High-performance Audio Codec - What Chip Designers Need to Know
- Density Management in Analog Layout Design: Addressing Issues and Ensuring Consistency
- Nexus: A Lightweight and Scalable Multi-Agent Framework for Complex Tasks Automation
Most Popular
- System Verilog Assertions Simplified
- System Verilog Macro: A Powerful Feature for Design Verification Projects
- Synthesis Methodology & Netlist Qualification
- Discover new Tessent UltraSight-V from Siemens EDA, and accelerate your RISC-V development.
- Understanding Logic Equivalence Check (LEC) Flow and Its Challenges and Proposed Solution