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
