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
212-620-7300
www.adacore.com

Altran Praxis Ltd.
Bath, England
+44 (0)1225 466991
www.altran-praxis.com

ASTA USA
Boise, Idaho
866-446-1860
www.asta-usa.com

Atlassian
San Francisco
415-701-1110
www.atlassian.com

Boston Business Computing Ltd.
Acton, Mass.
978-725-3222
www.bosbc.com

Concept Engineering GmbH
Freiburg, Germany
+49-761-47094-0
www.concept.de

Coverity Inc.
San Francisco
415-321-5200
www.coverity.com

DDC-I Inc.
Phoenix
602-275-7172
www.ddci.com

Digital Rapids
Markham, Ontario
905-946-9666
www.digital-rapids.com

Discover Video
Wallingford, Conn.
203-626-5267
www.discovervideo.com

Green Hills Software
Santa Barbara, Calif.
805-965-6044
www.ghs.com

Guzik Technical Enterprises
Mountain View, Calif.
650-625-8000
www.guzik.com

Intel Corp.
Santa Clara, Calif.
408-765-8080
www.intel.com

James Heires Consulting Inc.
Cedar Rapids, Iowa
319-551-2825
www.jamesheiresconsulting.com

KLOCwork Inc.
Burlington, Mass.
866-556-2967
www.klocwork.com

LDRA Ltd.
Wirral, England
0151 649 9300
www.ldra.com

LynuxWorks Inc.
San Jose, Calif.
408-979-3900
www.lynuxworks.com

The MathWorks Inc.
Natick, Mass.
508-647-7001
www.mathworks.com

Obsidian Software Inc.
Austin, Texas
512-330-9818
www.obsidiansoft.com

Open Controller
Berlicum, The Netherlands
+ 31 (0)73 6449992
www.opencontroller.com

Programming Research Inc.
Boston
617-273-8448
www.programmingresearch.com

Reasoning LLC
Raleigh, N.C.
866-379-6618
www.reasoning.com

Scientific Toolworks Inc.
St. George, Utah
435-627-2529
www.scitools.com

Taurus teleSYS Inc.
Newport News, Va.
757-873-2700
www.tgate.com

TESTCo Inc.
Del Valle, Texas
888-254-9709
www.testco.com

Wind River Systems Inc.
Alameda, Calif.
510-748-4100
www.windriver.com

XGC Software
Farnborough, England
011 44 1483 433312
www.xgc.com




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

XPand6020 | Small Form Factor (SFF) System Featuring XPedite5205 Running Cisco IOS® and XPedite7450

The XPand6020 is a Small Form Factor (SFF) system that features an XPedite5205, which runs Cisco ...

XPand1400 Series | Development Platform For XPand6000 Series, X-ES COM Express® Modules, and PMC/XMC Modules

The XPand1400 Series COM Express Development Platform targets the X-ES Small Form Factor (SFF) XP...

XPort3200 | Freescale QorIQ P1020 Processor-Based Conduction- or Air-Cooled XMC/PMC IEEE 1588v2 Grandmaster Clock Module

The XPort3200 is a rugged, IEEE 1588v2 Precision Time Protocol (PTP) ordinary clock with grandmas...

XPedite5205 | Embedded Services Router (ESR) with Cisco IOS® on an XMC/PMC Module

The XPedite5205 XMC/PMC-based Embedded Services Router (ESR) router runs Cisco IOS® Software with...

XPedite7472 | Intel® Core™ i7 Processor-Based Conduction- or Air-Cooled 3U VPX-REDI SBC with SecureCOTS™

The XPedite7472 is a secure and high-performance, 3U VPX-REDI, single board computer based on the...

XChange3013 | 3U VPX Gigabit Ethernet Switch with Optional Layer 2 Switching and Layer 3 Routing Management Support

The XChange3013 is a conduction- or air-cooled, 3U VPX Ethernet switch module. The XChange3013 pr...

XPand3200 Series | Sub-½ ATR, Conduction-Cooled Systems Supporting Conduction-Cooled Modules

The XPand3200 Series redefines the limits of power, performance, and functionality in a sub-½ ATR...

XPort5005 | XMC Form Factor PCIe Mini Card Carrier Board

The XPort5005 is an XMC module that can be quickly configured to support a platform’s specific I/...

XPedite5401 | Freescale Eight-Core P4080 Conduction-Cooled PrPMC/XMC Module with Two GbE Ports

The XPedite5401 is a high-performance PrPMC/XMC, single board computer supporting Freescale QorIQ...

XPedite7501 | 5th Generation Intel® Core™ i7 Broadwell-H Processor-Based Conduction- or Air-Cooled XMC Module

The XPedite7501 is a high-performance, low-power, XMC module based on the 5th generation Intel® C...

Related Companies

General Atomics Aeronautical Systems Inc

GA-ASI is a leading manufacturer of proven, reliable Remotely Piloted Aircraft (RPA) systems, radars, and electro-opt...

DiCon Fiberoptics Inc

Offers fiber optic switches, tunable filters, and VOAs. Founded in 1986, the company is a US based, AS9100 certified,...

Curtiss-Wright Defense Solutions

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

DDC-I Inc

Offers complete solutions for embedded software developers with a focus on mission- and safety-critical applications....

Harris Corporation

Harris provides advanced, technology-based solutions that solve government and commercial customers' mission critical...

United Electronic Industries Inc

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

Crane Aerospace & Electronics

When failure is NOT an option...rely on Crane Aerospace & Electronics. We supply high-density, high-reliability c...

MERITEC

Signal integrity leaders and preferred vertically integrated manufacturer of high-performance electrical and electron...

AcQ Inducom

Develops and produces non-certified and certified high-tech modular hardware- and software solutions for on-board and...

Advanced Conversion Technology Inc

ACT designs and manufactures, since 1981, an extensive range of AC-DC and DC-DC power supplies (switching, linear, ra...
Wire News provided by   

Press Releases

Model INCX-4001

The INCX-4001 consists of a high quality audio transceiver specifically designed to implement a complete fiber optic intercom.

Model PS-1210

The PS-1210 is a 1A, 12VDC stand-alone or rack mountable non-switcher (no RF noise) power supply.

Model OS-3121

Optical switches are utilized to disconnect, bypass and reroute fiber optic communications. All of these optical switches are purely optical path, there is no optical to e...

Webcasts

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:

All Access Sponsors


Mil & Aero Magazine

June 2015
Volume 26, Issue 6
file

Download Our Apps



iPhone

iPad

Android

Follow Us On...



Newsletters

Military & Aerospace Electronics

Weekly newsletter covering technical content, breaking news and product information
SUBSCRIBE

Cyber Security

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

Defense Executive

Monthly newsletter covering business news and strategic insights for executive managers
SUBSCRIBE

Electronic Warfare

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

Embedded Computing Report

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

Unmanned Vehicles

Monthly newsletter covering news updates for designers of unmanned vehicles
SUBSCRIBE