U.S. Department of Transportation
Federal Highway Administration
1200 New Jersey Avenue, SE
Washington, DC 20590
2023664000
Federal Highway Administration Research and Technology
Coordinating, Developing, and Delivering Highway Transportation Innovations
This report is an archived publication and may contain dated technical, contact, and link information 

Publication Number: FHWARD04080
Date: September 2004 
Software Reliability: A Federal Highway Administration Preliminary HandbookPDF Version (697 KB)
PDF files can be viewed with the Acrobat® Reader® Alternative Text for Images and FiguresFiguresFigure 1. The V (U) Model for SDLC. Diagram. This figure shows an inverted triangle, in the shape of a V, to demonstrate the phases of the software development life cycle. At the top left of the V is a box that reads, “Requirements.” Following a path down the left side of the V, subsequent boxes read, “Specifications,” “Design High Level,” “Unit Design Low Level,” and “Build Code” at the bottom of the V. Continuing up the right side of the V, the boxes read, “Unit Testing,” “Integration Testing,” “System Testing,” and “Acceptance Testing.” Figure 2. Simplified V Model with Handbook Techniques. Diagram. This simplified V model contains only five phases within the V shape. Beginning at the top left of the V, these are, in sequential order, “Functional Requirements and Specifications,” “High and LowLevel Design,” “Construction Code,” “Integration and Unit Testing,” and “Acceptance and System Testing.” An icon representing SpecChek is at the top of the figure, and arrows point from the icon to the first and last phases in the V (“Functional Requirements and Specifications” and “Acceptance and System Testing”). At the next level down, an icon representing Wrapping is in the middle of the V, and arrows point from this icon to the last two phases, “Integration and Unit Testing,” and “Acceptance and System Testing.” Below this level, an icon represents Numerical Reliability, and it points upward to the “Integration and Unit Testing” phase. Finally, two arrows begin at the “Functional Requirements and Specifications” and “High and LowLevel Design” phases directly across to the “Integration and Unit Testing” and “Acceptance and System Testing” phases, respectively. Figure 3. Model of SpecChek Method. Diagram. There are three sets of boxes in this figure. The first box contains three smaller boxes: “Specifications,” which points to “Software Development, Design, …Implementation,” which points to “Software System.” The second box contains two smaller boxes: “Input” and “Output.” A line leads from the arrow between “Software Development, Design,…Implementation” and “Software System” to the “Input” box, and an arrow leads from the “Software System” box to the “Output” box. The third box contains two smaller boxes: “DT Development” and “SpecChek Interpreter: SpecChek Code, XML Library, and Java Runtime Environment.” An arrows leads from the “Specifications” box into the “DT Development” box, and another arrow leads from the “Input” box to the entire third box. An arrow leads out of this third box to the words, “Specifications Satisfaction.” Figure 4. Checking Software with SpecChek. Diagram. From the left top of the diagram, an arrow leads to the words, “Specifications Satisfaction.” If yes, an arrow continues to a box below, “Software Correctness with High Confidence Level.” If no, an arrow leads to two boxes and the word Or is between the two boxes indicating either one if no. The first box contains two smaller boxes: “DT Development” and “SpecChek Interpreter: SpecChek Code, XML Library, and Java Runtime Environment.” The second box reads “Software System.” EquationsEquation 1. The sum of the set A to B of probability P times a given probability density function, observed P, times DP. Equation 2. The sum of the set 0 to 1 of probability P times observed P times DP. Equation 3. P when the observed value of P is in set A, B equals the quotient of the following: the sum of the set A to B of probability P times observed P times DP divided by the sum of the set 0 to 1 of probability P times observed P times DP. Please confirm. Equation 4. The sum of the set A to B of probability P0 of P times Q raised to the N power times DP divided by the sum of the set 0 to 1 of probability P0 of P times Q raised to the N power times DP. Equation 5. The sum of the set A to B of Q raised to the N power times DP divided by the sum of the set 0 to 1 of Q raised to the N power times DP. Equation 6. The sum of the set A to B of Q raised to the N power times DP equals the quotient of the following: the sum of 1 minus A raised to the N plus 1 power minus the sum of 1 minus B raised to the N plus 1 power, all divided by N plus 1. Equation 7. The sum of the set 0 to 1 of Q raised to the N power times DP equals 1 divided by N plus 1. Equation 8. The sum of the set A to B of Q raised to the N power times DP equals the quotient of the following: 1 minus the sum of 1 minus B raised to the N plus 1 power, all divided by N plus 1. Equation 9. P, when P is less than or equal to B with N successes equals 1 minus the sum of 1 minus B raised to the N plus 1 power, all divided by N plus 1. Please confirm that this is correct. Equation 10. Q raised to the power of N plus N times P times Q raised to the power of N minus 1. Equation 11. The sum of the set 0 to 1 of the product of 1 minus the sum of 1 minus P raised to the uppercase N power, all times P times P, N, times DP divided by the sum of the set of 0 to 1 of P times P, N, times DP. Equation 12. 1 minus P, all raised to the N power. Equation 13. The sum of the set 0 to 1 of the product of 1 minus the sum of 1 minus P raised to the N power, minus the sum of 1 minus P raised to the uppercase N plus N power, times DP equals the quotient of the following: quotient of 1 divided by the sum of N plus one, minus the quotient of 1 divided by the sum of uppercase N plus N plus 1, all divided by the quotient of 1 divided by the sum of N plus 1. This equals 1 minus the quotient of the sum of N plus 1 divided by the sum of uppercase N plus N plus 1. Equation 14. 0.5 is equal to or less than 1 minus the quotient of the sum of N plus 1 divided by the sum of uppercase N plus N plus 1. Equation 15. 0.5 times the sum of uppercase N plus N plus 1 is equal to or less than 1 minus N minus 1. Equation 16. P equals 1 minus the quotient of the sum of N plus 1 divided by the sum of 1001 times N plus 1. Equation 17. The relative error of X equals the quotient of the absolute value of the sum of FL of X minus X divided by X, for a pure mathematical number X does not equal 0. Equation 18. The absolute value of the sum of FL of X minus X, all divided by X. Equation 19. The relative error of X is less than or equal to U. Equation 20. U equals B divided by 2 times B raised to the negative T power, which equals B raised to the 1 minus T power divided by 2. Equation 21. Onehalf times 10 raised to the negative T minus 1 power equals onehalf times 10 raised to the 1 minus T power. Equation 22. U equals 5 times 10 raised to the negative 15 power. Equation 23. The relative error of the FL of X OP Y is less than or equal to U. Equation 24. The relative error of the FL of X OP Y is less than or equal to X OP Y times the sum of 1 plus U. Equation 25. FL of X OP Y equals X OP Y times the sum of 1 plus E. Equation 26. FL of X equals X divided by 1 plus E. Equation 27. D squared divided by 12. Equation 28. 2 times U squared divided by 12. Equation 29. FL of A times E of A plus FL of B times E of B plus E1 times the sum of FL of A plus FL of B. Equation 30. VAR of C1 times E1 plus C2 times E2 equals FABS of C1 times VAR of E1 plus FABS of C2 times VAR of E2. Equation 31. V times the sum of A plus B equals FABS of FL of A times V of A plus FABS of FL of B times V of B plus FABS of the sum of FL of A plus FL of B times V of E1. Equation 32. V of E1 equals the product of 2 times U, squared, all divided by 12. Equation 33. ME times the sum of A plus B equals FABS of FL of A times ME of A plus FABS of FL of B times ME of B plus FABS of the sum of FL of A plus FL of B times ME of E1. Equation 34. VAR of C1 times E1 minus C2 times E2 equals FABS of C1 times VAR of E1 plus FABS of C2 times VAR of E2. Equation 35. V times the sum of A minus B equals FABS of FL of A times V of A plus FABS of FL of B times V of B plus FABS of the sum of FL of A minus FL of B times V of E1. Equation 36. ME times C1 times E1 minus C2 times E2 equals FABS of C1 times ME of E1 plus FABS of C2 times ME of E2. Equation 37. ME times the sum of A minus B equals FABS of FL of A times ME of A plus FABS of FL of B times ME of B plus FABS of the sum of FL of A minus FL of B times ME of E1. Equation 38. A equals 0.D1 times D2 through the set DT times B superscript E. Equation 39. Plus or minus U prime equals onehalf times B raised to the 1 minus the sum of T minus K power. Equation 40. Plus or minus U prime equals onehalf times B raised to the 1 minus T power. Equation 41. VAR of A times B equals FABS of FL of A times FL of B times VAR of E1 plus VAR of E times A plus VAR of E times B. Equation 42. ME of A times B equals FABS of FL of A times FL of B times ME of E1 plus ME of E times A plus ME of E times B. Equation 43. VAR of A divided by B equals FABS of FL of A divided by FL of B times VAR of E1 plus VAR of E times A plus VAR of E times B. Equation 44. ME of A divided by B equals FABS of FL of A divided by FL of B times ME of E1 plus ME of E times A plus ME of E times B. Equation 45. FABS of C1 times VAR of E times A plus FABS of C2 times VAR of E times B plus FABS of C3 times VAR of E1. Equation 46. FABS of C1 times ME of E times A plus FABS of C2 times ME of E times B plus FABS of C3 times ME of E1. Equation 47. FL of (A plus B) plus C minus A plus B plus C equals the sum of A plus B times the sum of 1 plus E1, plus C, all times the sum of 1 plus E2, minus A plus B plus C, equals the sum of A plus B times the sum of E1 plus E2, plus the product of C times E2. Equation 48. FL of (A plus B) plus C minus A plus B plus C equals the sum of B plus C times the sum of E1B plus E2B, plus the product of AC times E2B. Equation 49. FL of (A plus B) plus C exclamation point (is this correct here?) equals FL of A plus (B plus C). Equation 50. Error equals ArgVector times ErrorVector. Equation 51. The absolute value of E is less than or equal to U, which equals 5 times B top hat, top hat, negative T. Equation 52. 2 times U top hat, top hat, 2 divided by 12 equals 2 times 5 times E minus 15 top hat, top hat 2 divided by 12, which equals 100E minus 30 divided by 12, or approximately E minus 27. Chapter 5long factorial( int n) { long result = 1; if (n < 1) { printf( "Error  factorial input should be positive.\n"); return 0; } else if (n == 1) return 1; while (n>0) { result = result * n; n; } return result; } long factorial( int n) { if (n<1) { printf( "Error  factorial input should be positive.\n"); return 0; } else if (n == 1) return 1; else return n * factorial(n1); } Chapter 6float big; big=0.0; for(j=1;j<=n;j++) {if((temp=fabs(a[i1][j1])) > big) big=temp; } if (big==0.0) Error("singular matrix",1); int wrapped_inverse( double * in, double ** out, int dim) { double * possible_inverse; double * possible_identity; double * identity; inverse( in, &possible_inverse, dim); multiply( in, possible_inverse, &possible_identity, dim); identity( &identity, dim); if (distance( identity, possible_identity) > EPSILON ) return(0); multiply( possible_inverse, in, &possible_identity, dim); if (distance( identity, possible_identity) > EPSILON ) return(0); else return(1); } int fact( int j) { int temp; if (j<0) return(0); else if (j<2) return(1); else { printf("asking for fact(%d)\n",j1); temp = fact(j1); printf("j=%d, fact(j) = %d\n",j1,temp); return( temp*j ); } } int wrapped_fact( int j, int * flag) { int fn_result; float float_fn_result; int comparison; fn_result = fact(j); float_fn_result = ffact(j); *flag = (fabs(fn_resultfloat_fn_result)< EPSILON); printf("Inside wrapped_fact, arg = %i, *flag=%i\n", j,*flag); return(fn_result); } int wrapped_fact( int j, int * flag) { int temp_fn_result; int fn_result; float float_fn_result; if (j<2) return(1); else { printf("asking for fact(%d), *flag=%i\n",j1, *flag); temp_fn_result = wrapped_fact(j1, flag); printf("j=%d, fact(j) = %d *flag=%i\n", j1,temp_fn_result, *flag); if (*flag) { fn_result = j * temp_fn_result ; float_fn_result = j * (float)temp_fn_result ; /* TYPE CAST IS NEEDED HERE */ *flag = *flag && (fabs(fn_resultfloat_fn_result)< EPSILON); printf("fact(%d)=%d, ffact=%f, *flag=%d\n", j,fn_result,float_fn_result,*flag); } else fn_result = j * fn_result ; } return(fn_result); } int driver( int j) { int cumulative_result = 1; int single_result ; int fn_result; int i; printf("Inside driver testing fact:\n"); for (i=1; i<=j && cumulative_result; i++) { fn_result = wrapped_fact(i, &single_result); cumulative_result= cumulative_result && single_result; printf("PARTIAL RESULT FROM DRIVER:\n"); printf("Argument fn. value, correct flag, cum correct flag\n"); printf("%i %i %i %i\n", i, fn_result, single_result, cumulative_result ); } return( cumulative_result ); } int main() { int result; /* result of driver */ int j; /* scope is main */ printf("Enter an positive integer.\n"); printf(">>"); scanf("%d", &j); if (j>=1) { result = driver(j); if (result) printf("*****RESULT OF %i FACTORIALS IS TRUE", j); else printf("*****RESULT OF %i FACTORIALS IS FALSE", j); } return(0); } <and> <text> topic1, ... topicN </text> </and> <and> <and><text> topic1</text></and> ... <and><text> topicN</text></and> </and> <and> <text> if P1 then text1 if P2 then text2 ... otherwise textN </text> </and> <ifthenelse> <ifthen> <if> <text> P1 </text> </if> <then> <text> text1 </text> </then> </ifthen> <ifthen> <if> <text> P2 </text></if> <then> <text> text2 </text> </then> </ifthen> .... <else> <text> textN </text> </else> </ifthenelse> <and><text>text(R1...RN) </text> </and> into <and> <and><text> text(R1) </text> </and> ... <and><text> text(RN) </text> </and> </and> <or> <and><text> text(R1) </text> </and> ... <and><text> text(RN) </text> </and> </or> <?xml version="1.0"?> <!DOCTYPE specs SYSTEM "specs2.dtd"> <! 0.1 specs.xml > <specs name ="consistency"> <or name = "top" level = "0"> <ifthen level = "1" name = "ifthen1" > <if name = "if1" level = "2"> <test name = "test1"> inHorizCurve == true </test> </if> <then> <action>goto horizontal</action> </then> </ifthen> <ifthen level = "1" name = "ifthen2"> <if><and> <test> inHorizCurve == true <test> inVertCurve == true </and> </if> <then> <action>goto verticalonhoriz</action> </then> </ifthen> <ifthen level = "1" name = "ifthen3"> <if><and> <test> inHorizCurve == false <test> inVertCurve == true </and></if> <then> <action>goto AC6</action> </then> </ifthen> </or> <or name = "horizontal" level ="0"> <ifthen level = "1" name = "ifthen4"> <if> <test> Grade LT 4.0 </if> <then> <test>V85 == 102.10  3077.13 \ R tol 0.001 <! <action>goto AC1 > </then> </ifthen> <ifthen level = "1" name = "ifthen5"> <if><and> <test>Grade GE 4.0</test> <test>Grade LT 0.0</test> </and> </if> <then> <test> V85 == 105.98  3709.90 \ R tol 0.001</test> <! <action>goto AC2</action> > </then> </ifthen> <ifthen level = "1" name = "ifthen6"> <if><and> <test>Grade GE 0.0</test> <test>Grade LT 4.0</test> </and></if> <then> <test> V85 == 104.82  3574.51 \ R tol 0.001</test> <! <action>goto AC3</action> > </then> </ifthen> <ifthen level = "1" name = "ifthen7"> <if> <test>Grade GE 4.0</test> </if> <then> <test> V85 == 96.61  2752.19 \ R tol 0.001</test> <! <action>goto AC4</action> > </then> </ifthen> </or> <or name = "verticalonhoriz" level ="0"> <ifthen level = "1" name = "ifthen8"> <if> <test>PVCbeforeMP == true</test> <then level = "2"> <action level = "3">A = abs(G1  G2) </action> <! Absolute value difference between entering and departing grades > <action level = "3">Ym = A * L \ 800 </action> <! midcurve offset > <action level = "3">PVIelev = PVCelev + ((G1\100) * (L\2)) </action> <! elevation at point of vertical intersection > <action level = "3">MVCelev = PVIelev  Ym <! elevation at midpoint of vertical curve > </action> <! crest  for a sag its: + Ym > <action level = "3">EG = (MVCelev  PVCelev)\(L\2)</action> <action level = "3">Grade = EG </action> <action level = "3">goto horizontal </action> </then> <! level 2 > </ifthen> <! level 1 > <ifthen level = "1" name = "ifthen9"> <if> <test>PVCbeforeMP == false</test> </if> <then> <action>goto AC5B</action> </then> </ifthen> </or> </specs> newDataSet = 0 Grade = 0.3845 inVertCurve = true inHorizCurve = true R = 300.0 L = 161.44419999999997 PVCelev = 43.1482 G2 = 2.5367 G1 = 0.3845 PVCbeforeMP = true Grade = 0.0016840677966101707 inVertCurve = false inHorizCurve = true R = 175.0 L = 149.66250000000002 PVCelev = 39.4976 G2 = 0.0 G1 = 0.0016840677966101707 The top level tree consistency is false because The or node top is false, because no subnode was satisfied. This is because The ifthen node ifthen1 fails, because The Then node 1th then subnode of ifthen1 fails, because 2th action subnode of 1th then subnode of ifthen1 goto horizontal was NOT successfully executed.This is because The or node horizontal is false, because no subnode was satisfied. This is because The ifthen node ifthen5 fails, because The Then node 1th then subnode of ifthen5 fails, because Relation 1th test subnode of 1th then subnode of ifthen5: The relation V85 == 105.98  3709.90 \ R tol 0.001 is false. It is evaluated as 93.11366667 == 93.61366666666667 tol 0.0010. . The ifthen node ifthen2 fails, because The Then node 1th then subnode of ifthen2 fails, because 1th action subnode of 1th then subnode of ifthen2 goto verticalonhoriz was NOT successfully executed.This is because The or node verticalonhoriz is false, because no subnode was satisfied. This is because The ifthen node ifthen8 fails, because The Then node 1th then subnode of ifthen8 fails, because 7th action subnode of 1th then subnode of ifthen8 goto horizontal was NOT successfully executed.This is because The or node horizontal is false, because no subnode was satisfied. This is because The ifthen node ifthen5 fails, because The Then node 1th then subnode of ifthen5 fails, because Relation 1th test subnode of 1th then subnode of ifthen5: The relation V85 == 105.98  3709.90 \ R tol 0.001 is false. It is evaluated as 93.11366667 == 93.61366666666667 tol 0.0010. 
Topics: research, safety, data and analysis tools Keywords: research, safety, software reliability, roundoff errors, floating points errors, software verification and validation, software testing, SpecChek TRT Terms: Computer softwareReliability, Computer softwareVerification, Computer softwareValidation, Highway engineering, Highway design, Highway safety, Software, Validation Updated: 03/08/2016
