New version page

Infinite State Model Checking

Upgrade to remove ads

This preview shows page 1-2-24-25 out of 25 pages.

Save
View Full Document
Premium Document
Do you want full access? Go Premium and unlock all 25 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 25 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 25 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 25 pages.
Access to all documents
Download any document
Ad free experience

Upgrade to remove ads
Unformatted text preview:

Analyzing Tabular Requirements Specifications Using Infinite State Model CheckingOutlineSlide 3Slide 4Slide 5Action Language Tool SetComposite Symbolic LibraryComposite Symbolic Library, ExtendedComposite Symbolic Library, Further ExtendedSCR to Action LanguageSlide 11Slide 12Two Example SCR SpecificationsVerification of InvariantsTransition InvariantsConsistency Checking with ALVSlide 17Use of Multiple Symbolic RepresentationsExplicit vs. Symbolic Model CheckingFinite vs. Infinite State Model CheckingParameterized VerificationAbstraction and Symbolic RepresentationInvariant GenerationModel Checking vs. Theorem ProvingConclusionsAnalyzing Tabular Requirements Specifications Using Infinite State Model CheckingTevfik BultanUniversity of California, Santa BarbaraConstance HeitmeyerNaval Research LaboratoryOutline•SCR Toolset•Action Language Verifier•SCR to Action Language•Two Examples•ExperimentsHISTORY OFSCR SCR APPROACH1978: Heninger,Parnas+ publish A-7/SCR requirements documentTabular notation Events and conditionsMode classes and terms1980s-early 1990s: SCR applied to a wide range of systemsTelephone networks (AT&T Bell Labs)Submarine communications (NRL) Control software for nuclear plants (Ontario Hydro)Avionics software (Grumman)Early 1990s: Development of Four Variable Model and CoREParnas+ introduce and apply Four Variable ModelSoftw. Productivity Consortium develops CoRE method (based on SCR)Lockheed applies CoRE and SCR tables to C-130J flight program 1994-present: NRL develops formal SCR model and toolsSCR SCR SSoftware C Cost R ReductionSPECIFY THE SYSTEMPRECISELYUse a TABULARTABULARnotation with anexplicit formal semantics to specify therequired behaviorAPPLY“CONSISTENCYCHECKING”Automatically check spec forsyntax/type errors,missing cases,nondeterminism,circular defs, etc.SIMULATETHESYSTEM BEHAVIORSymbolicallyexecute the system basedon the (executable) req. specsSCRSCR GOAL: MAKE ‘FORMALMETHODS’ PRACTICAL As we move down the chain, we increaseassurance in the specINCREASING EFFORT, INCREASED EXPERTISEVERIFYSPECS USINGTHEOREM PROVINGVERIFYSPECS USINGMODEL CHECKINGCheckcriticalapplicationproperties• Usable, scalable tabular notation• Integrated set of robust software tools– light-weight tools whose use does not require math. sophistication/thm proving– heavy-duty tools (e.g., theorem prover)SCR REQUIREMENTS TOOLSETSCR REQUIREMENTS TOOLSET THEOREM PROVER(TAME)INVARIANTGENERATORMORE MORE ANALYSIS ANALYSIS TOOLSTOOLSSCR BASICSCR BASICTOOLSTOOLSPROPERTYCHECKER (Salsa)CONSISTENCYCHECKER DEPENDENCYGRAPH BROWSERSPECIFICATIONEDITORMODEL CHECKERSIMULATOR•Designed to help a developer specify and analyze requirements•most mature tools•installed at 200+ organizations in industry, govt., and academia•TAME - interface to PVS designed to prove properties of state machine modelsTEST CASE GENERATORSOURCE CODE GENERATORResearch Prototypes Research Prototypes Produces optimized C & Java codeProduces optimized C & Java coderequirements specmodeseventsmon varscont varsconditionstermsAction Language Tool SetAction Action LanguageLanguageParserParserAction Action LanguageLanguageVerifierVerifierOmega Omega LibraryLibraryCUDDCUDDPackagePackageMONAMONAComposite Symbolic LibraryComposite Symbolic LibraryPresburgerPresburgerArithmeticArithmeticManipulatorManipulatorBDDBDDManipulatorManipulatorAutomataAutomataManipulatorManipulatorAction Action LanguageLanguageSpecificationSpecificationVerifiedVerifiedCounter Counter exampleexample•A symbolic CTL model checker•Supports infinite state model checking–unbounded integer variables, Presburger arithmetic•Composite symbolic representation:–Polyhedra and automata representation for Presburger arithmetic, BDDs for Boolean and bounded variables, shape graphs for heap variables•Uses conservative approximations for fixpoints –widening and truncated fixpoints•Supports parameterized verification–parameterized constants–parameterized modulesComposite Symbolic LibraryCUDD Library OMEGA LibrarySymbolic+intersect()+union()+complement()+isSatisfiable()+isSubset()+pre()+post() CompSym–representation: list of comAtom +intersect()+ union() • • •BoolSym–representation: BDD+intersect()+union() • • •IntSym–representation: Polyhedra+intersect()+union() • • •compAtom–atom: *SymbolicComposite Symbolic Library, ExtendedOMEGA LibrarySymbolic+union()+isSatisfiable()+isSubset()+forwardImage() CompSym–representation: list of comAtom + union() • • •compAtom–atom: *SymbolicIntSymAuto–representation: automaton+union() • • •IntSym–representation: list of Polyhedra+union() • • •CUDD LibraryBoolSym–representation: BDD+union() • • •MONAIntBoolSymAuto–representation: automaton+union() • • •Composite Symbolic Library, Further ExtendedCUDD Library OMEGA LibrarySymbolic+union()+isSatisfiable()+isSubset()+forwardImage() CompSym–representation: list of comAtom + union() • • •BoolSym–representation: BDD+union() • • •compAtom–atom: *SymbolicHeapSym–representation: list of ShapeGraph+union() • • •IntSym–representation: list of Polyhedra+union() • • •ShapeGraph–atom: *SymbolicSCR to Action Language•SCR: Tabular specifications –Mode transition tables–Condition tables–Event tables•Events–@T(c) = c  c’ •In Action Language: !c and c’ –@T(c) WHEN d =  c  c’  d•In Action Language: !c and c’ and dSCR to Action Language•Each row in an SCR table can be translated to a formula on current and next-state variables•The transition relation of a table is defined by the disjunction of the formulas that correspond to its rows•The transition relation of the whole system is defined by the conjunction of the transition relations of its tables•The initial expression in Action Language is used to define the initial states•The restrict expression in Action Language is used to restrict the domains of the variables according to their type definitionsSCR to Action Languagemodule main() enumerated CruiseCtrl {Off, Inactive, Cruise, Override}; boolean IgnOn; enumerated Throttle { accel, maintain, decel, off }; initial: CruiseMode=Off and !IgnOn and


Download Infinite State Model Checking
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Infinite State Model Checking and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Infinite State Model Checking 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?