Mathematical proof techniques, automated requirements tracing lead trends in software verification tools

Click to EnlargeBy John Keller

Product intelligence, 5 July 2011. Complex application software increasingly is finding its way into mission- and life-critical applications like medical equipment, surveillance and reconnaissance systems, and even high-end passenger cars. Despite the importance of this software, however, much of today's sophisticated code is developed in somewhat of a haphazard manner with little fool-proof debugging going on, and even less code verification based on formal methods.

"The modern car has more lines of code than a typical commercial jetliner," says Robert Dewar, president and chief executive officer of AdaCore Technologies Inc. in New York. "Medical instrumentation has critical software that also is written in a haphazard way," he says.

Software in these kinds of mission- and life-critical systems could learn a thing or two from aerospace and defense technology, such as avionics and military systems in which formal certification is mandatory, and where the use of software verification tools are seeing increasing use not only to find software bugs, but also to exercise the software automatically in a wide variety of scenarios to ensure the code will work every time.

Approaches to software verification tools are widely varied, but tend to segment into static tools, which work with the source code itself, and dynamic test tools, which execute the code with test cases to verify that the software works correctly. New kinds of dynamic software code verification tools seek to automate the process of following software verification requirements.

In addition, software engineers are working on developing formal, mathematical proof techniques to ensure code quality. Among the companies invested in formal mathematical proof techniques for software code verification is The MathWorks in Natick, Mass.

"There is a new class of verification tools that actually analyzes the code to check to make sure there won't be a certain class of runtime errors," says Jon Friedman, aerospace and defense industry marketing manager at The MathWorks. "These check to make sure that the engineer hasn't left openings for those kinds of problems."

Formal, mathematically provable methods are absolutely essential for removing all doubt that software will work when called on, says Jay Abraham, product marketing manager at The MathWorks. "You cannot do exhaustive software testing without formal methods," Abraham says. "Formal mathematics can boil down these complicated problems into smaller problems that you can prove."

AdaCore's Dewar says use of mathematical proof techniques is a major trend in software verification tools today. He says this technology should be mature within the next five years. "It is being used today, but it is not yet standard industry practice," Dewar says.

Today's high-performance and relatively inexpensive computing is helping software engineers implement formal methods in software code verification. In years past, the kind of computing necessary to run formal methods was unavailable to most engineers.

Following a set process for software code verification is not new, but in the recent past has been a laborious process. Today, software engineers are trying to automate that process of tracing requirements all the way down to testing on a target, says Chris Murray, vice president of business development at LDRA Ltd. U.S. office in San Bruno, Calif.

"It is most important to be able to find out which software artifact is connected upstream or downstream to another artifact," Murray says. "You need to do that quickly and efficiently. LDRA does that with a tool called Object Box, which is a component of the LDRA Tool Suite that includes static and dynamic software testing and requirements traceability.

Company information

AdaCore Technologies Inc.
New York

Altran Praxis Ltd.
Bath, England
+44 (0)1225 466991

Boise, Idaho

San Francisco

Boston Business Computing Ltd.
Acton, Mass.

Concept Engineering GmbH
Freiburg, Germany

Coverity Inc.
San Francisco

DDC-I Inc.

Digital Rapids
Markham, Ontario

Discover Video
Wallingford, Conn.

Green Hills Software
Santa Barbara, Calif.

Guzik Technical Enterprises
Mountain View, Calif.

Intel Corp.
Santa Clara, Calif.

James Heires Consulting Inc.
Cedar Rapids, Iowa

KLOCwork Inc.
Burlington, Mass.

Wirral, England
0151 649 9300

LynuxWorks Inc.
San Jose, Calif.

The MathWorks Inc.
Natick, Mass.

Obsidian Software Inc.
Austin, Texas

Open Controller
Berlicum, The Netherlands
+ 31 (0)73 6449992

Programming Research Inc.

Reasoning LLC
Raleigh, N.C.

Scientific Toolworks Inc.
St. George, Utah

Taurus teleSYS Inc.
Newport News, Va.

Del Valle, Texas

Wind River Systems Inc.
Alameda, Calif.

XGC Software
Farnborough, England
011 44 1483 433312

Get All the Military Aerospace Electronics News Delivered to Your Inbox or Your Mailbox

Subscribe to Military Aerospace Electronics Magazine or email newsletter today at no cost and receive the latest information on:

  • C4ISR
  • Cyber Security
  • Embedded Computing
  • Unmanned Vehicles

Military & Aerospace Photos

Most Popular Articles

Related Products

XTend7103 | COM Express® Carrier for COM Express® Type 10 Mezzanine Modules

The XTend7103 is a COM Express® carrier card designed to provide a low-cost and compact platform ...

XPedite7575 | 5th Generation Intel® Core™ i7 Broadwell-H Processor-Based Conduction- or Air-Cooled 3U VPX-REDI Module

The XPedite7575 is a high-performance, 3U VPX-REDI, single board computer based on the 5th genera...

XPort6173 | 3U VPX Carrier for Two 2.5 in. Solid-State Drives (SSDs)

The XPort6173 supports two, standard, 2.5 in. Solid-State Drives (SSDs) in a single 0.8 in. or 1....

XPm2020 | 3U VPX Power Supply with Integrated MIL-STD-461E Filtering

The XPm2020 is a VITA 62-compliant 3U VPX power supply that takes in a MIL-STD-704 28 VDC input v...

XCalibur1645 | Freescale Eight-Core P4080 Processor-Based Conduction-Cooled 6U VPX Module

The XCalibur1645 is a high-performance, 6U VPX, single board computer supporting Freescale QorIQ ...

XPedite7479 | 3rd Gen Intel® Core™ i7 Processor-Based 3U VPX Module with Full XMC J16 I/O Routing

The XPedite7479 is a high-performance, low-power, 3U VPX-REDI, single board computer based on the...

XCalibur4443 | Intel® Core™ i7 Processor-Based Conduction-Cooled 6U VPX SBC

The XCalibur4443 is a high-performance, multiprocessing, 6U VPX, single board computer that is id...

XPm2120 | MIL-STD-704 3U VPX VITA 62.0 Power Supply with Integrated MIL-STD-461E Filtering

The XPm2120 is a VITA 62.0-compliant 3U VPX power supply that allocates 12 V as the primary distr...

XCalibur1740 | Freescale QorIQ P2020 Processor-Based Conduction- or Air-Cooled 6U VPX Module

The XCalibur1740 is a high-performance, multiprocessing, 6U VPX, single board computer that is id...

XCalibur4540 | 5th Generation Intel® Core™ i7 Broadwell-H Processor-Based Conduction- or Air-Cooled 6U VPX Module

The XCalibur4540 is a high-performance, 6U OpenVPX™, multiprocessing, single board computer that ...

Related Companies

Southwest Antennas

Designs and manufactures high-performance RF and Microwave antennas and accessories designed for today’s communicatio...

Curtiss-Wright Defense Solutions

About Curtiss-Wright Defense Solutions Curtiss-Wright Defense Solutions (CWDS) is a long established techno...

United Electronic Industries Inc

UEI is a leader in the PC/Ethernet data acquisition and control, Data Logger/Recorder and Programmable Automation Con...

Fabritech Inc

Fabritech was established in 1986 and specializes in the fabrication of EMI, RFI, and thermal shielded products made ...

NOVA Power Solutions Inc

Provides mission-critical rugged uninterruptable power supplies (UPS), power conditioners, and battery backup modules...

Sierra-Olympic Technologies Inc (SOTI)

Offers advanced infrared (IR) cameras (SWIR, MWIR, LWIR), thermal imaging components, MWIR/LWIR zoom optics and compl...


Spectracom supports mission-critical communications systems with precise and reliable time and frequency synchronizat...


Is a mechanical engineering consulting company headquartered in Los Angeles, CA with operations in Billerica, MA, pro...

Dspnor AS

Offers radar signal processing and distribution. The products interface to virtually any radar system in use today. T...


PALMARII Dynamics is a Swedish company incorporated in 2012 as a competence centre for specialist naval architecture ...


Harsh Environment Protection for Advanced Electronics and Components

This webinar will offer an opportunity to learn more about ultra-thin Parylene conformal coatings – how they are applied, applications they protect today, and the properties and benefits they offer, includin...

New Design Tools That Help You Develop Radar That Sees the Un-seeable and Detects the Undetectable

Xilinx EW/ISR System Architect, Luke Miller, has new tricks and he’s going to tell you all about them in a new Xilinx Webinar—for free. His Webinar will cover new ways to implement Radar functions including ...
Sponsored by:

Press Releases


Curtiss-Wright Corporation today announced that its Defense Solutions division has received a contract from Sierra Nevada Corporation (SNC) to supply its small form factor ...

Innovative Integration Announces the FMC-Servo

Camarillo, CA June 19, 2015, Innovative Integration, a trusted supplier of signal processing and data acquisition hardware and software solutions, today announced the FMC-S...


Curtiss-Wright Corporation today announced that its Defense Solutions division has further enhanced its innovative VRD1 high definition (HD) video management system (VMS) w...

All Access Sponsors

Mil & Aero Magazine

August 2015
Volume 26, Issue 8

Download Our Apps




Follow Us On...


Military & Aerospace Electronics

Weekly newsletter covering technical content, breaking news and product information

Cyber Security

Monthly newsletter covering cyber warfare, cyber security, information warfare, and information security technologies, products, contracts, and procurement opportunities

Defense Executive

Monthly newsletter covering business news and strategic insights for executive managers

Electronic Warfare

Quarterly newsletter covering technologies and applications in electronic warfare, cyber warfare, optical warfare, and spectrum warfare.

Embedded Computing Report

Monthly newsletter covering news on embedded computing in aerospace, defense and industrial-rugged applications

Unmanned Vehicles

Monthly newsletter covering news updates for designers of unmanned vehicles