11Testing Formal SpecificationsGCMPSC 266 March 12, 2009Testing Formal Specificationsand AslanTest2Testing Formal SpecificationsGCMPSC 266 March 12, 2009FormalSpecificationRequirementsHOL LanguageImplementationFormalModelInformal ReviewDesign VerificationCode verification3Testing Formal SpecificationsGCMPSC 266 March 12, 2009Formal Verification• Enables designer to show a systemis consistent with its requirements• Requirements are modeled using a precise formal model• System is specified and successively refined using a specification language• Proof obligations are generated to show consistency of specifications with requirements4Testing Formal SpecificationsGCMPSC 266 March 12, 2009The Problem• There may be no implementation that is consistent with the specification and provides the desired functionality• Often not discovered until the design has gone through several levels of refinement and proofyo-yo effect5Testing Formal SpecificationsGCMPSC 266 March 12, 2009Solution• Test the specifications• Specifications are nonprocedural• Two approaches– Rapid prototyping– Symbolic execution of the specifications6Testing Formal SpecificationsGCMPSC 266 March 12, 2009Rapid Prototyping• Convert the nonprocedural specification into procedural form• Procedural form serves as a rapid prototype• Test the rapid prototype27Testing Formal SpecificationsGCMPSC 266 March 12, 2009Symbolic Execution• Symbolically execute the operations• Check the resultant symbolic values to see if they define the desired set of resultant states8Testing Formal SpecificationsGCMPSC 266 March 12, 2009Functional Requirement (F)• Fstart – a start predicate that defines the set of states from which the sequence of operations can be invoked• SEQ – a sequence of operations to be executed in the specified order• Fresult – a resultant predicate that defines the set of states that satisfy the desired result after executing the sequence of ops9Testing Formal SpecificationsGCMPSC 266 March 12, 2009NotationLet• S be a formal specification• IMP(S) be all possible implementations of S• I(S) be an implementation of specification S• States(I) be the set of all possible states for implementation I10Testing Formal SpecificationsGCMPSC 266 March 12, 2009DefinitionsSatisfiability:F is satisfiable with respect to S if there exists an implementation of S that satisfies FUnsatisfiability:F is unsatisfiable with respect to S if none of the possible implementations of S satisfies FValidity:F is valid with respect to S if every possible implementation of S satisfies F11Testing Formal SpecificationsGCMPSC 266 March 12, 2009More FormallySatisfiability:F is satisfiable with respect to S if there exists an implementation of S that satisfies F(∃ I, I∈IMP(S)) (∀P, P∈STATES(I))(Fstart(P) −> Fresult(SEQ(P)))12Testing Formal SpecificationsGCMPSC 266 March 12, 2009More FormallyUnsatisfiability:F is unsatisfiable with respect to S if none of the possible implementations of S satisfies F(∀ I, I∈IMP(S)) (∃ P, P∈STATES(I))(Fstart(P) & ∼Fresult(SEQ(P)))313Testing Formal SpecificationsGCMPSC 266 March 12, 2009More FormallyValidity:F is valid with respect to S if every possible implementation of S satisfies F(∀ I, I∈IMP(S)) (∀P, P∈STATES(I))(Fstart(P) −> Fresult(SEQ(P)))14Testing Formal SpecificationsGCMPSC 266 March 12, 2009Rapid Prototype ToolInput– Formal specification– Start state of the system (i.e., variable values)or keyword DEFAULT– Sequence of transitions to be executedor keyword INTERACTIVE– Expected resultant state, a list of variables, or keyword ALL15Testing Formal SpecificationsGCMPSC 266 March 12, 2009Rapid Prototype Tool• Checks consistency of start state and invariant or if DEFAULT assigns program variable values that satisfy the invariant• Invokes the sequence of procedures or if INTERACTIVE then gets procedures from the user. Checks invariant after each procedure• Checks if resultant variable values satisfy the expected resultant state, prints out values of listed variables, or prints out the values of all variables16Testing Formal SpecificationsGCMPSC 266 March 12, 2009Symbolic Execution ToolInput– Formal specification– Start state of the system (i.e., predicate defining states) or keyword DEFAULT– Sequence of transitions to be executedor keyword INTERACTIVE– Expected resultant state (i.e., predicate defining desired resultant state) or keyword DEFAULT17Testing Formal SpecificationsGCMPSC 266 March 12, 2009Symbolic Execution Tool• Checks consistency of start state and invariant or if DEFAULT assigns specification variables values that satisfy the invariant• Symbolically executes the sequence of transitions or if INTERACTIVE then gets transitions from the user. Checks invariant after each transition• Checks if resultant state satisfies the expected resultant predicate or prints out the predicate that defines the resultant state18Testing Formal SpecificationsGCMPSC 266 March 12, 2009Rapid Prototype• Advantages– Helps the specification writer debug the specification– Helps a user experience the capabilities of the system– Errors are found earlier in the software life cycle• Disadvantages– Translating infinite domains– Nondeterministic specifications– Suffers all the disadvantages of testing– At best guarantees satisfiability419Testing Formal SpecificationsGCMPSC 266 March 12, 2009Symbolic Execution Tool• Advantages– Allows one to deal with infinite domains– Lets the user test a large number of test cases at one time– Helps the specification writer debug the specification– Errors are found earlier in the software life cycle• Disadvantages– May be difficult to glean pertinent information from resultant state– Predicates can get unmanageable20Testing Formal SpecificationsGCMPSC 266 March 12, 2009Symbolic Execution Tool• Consider transforms T1, T2, T3T1: (if A then B else C)T2: (if D then E else F)T3: (if G then H else I)What is the effect of executing the sequence T1,T2,T321Testing Formal SpecificationsGCMPSC 266 March 12, 2009Effect of T1,T2,T3(if G (if D (if A then B else C)then E (if A then B else C)else F (if A then B else C))then H (if D (if A then B else C)then E (if A then B else C)else F (if A then B else C))else I (if D (if A then B else C)then E (if A then B else C)else F (if A then B else C)))22Testing Formal SpecificationsGCMPSC 266 March 12, 2009AslanTest• A Symbolic Execution Tool for