View Full Document

Model Checking Accomplishments and Opportunities



View the full content.
View Full Document
View Full Document

2 views

Unformatted text preview:

Model Checking Accomplishments and Opportunities Rajeev Alur Systems Design Research Lab University of Pennsylvania www cis upenn edu alur Debugging Tools q Program Analysis Type systems pointer analysis data flow analysis q Simulation Effective in discovering bugs in early stages q Testing Expensive q Formal Verification Mathematical proofs Not yet practical Quest for Better Debugging q Bugs are expensive Pentium floating point bug Arian V disaster q Testing is expensive More time than design and implementation q Safety critical applications Certification mandated model temporal property Model Checker yes error trace Advantages Automated formal verification Effective debugging tool Moderate industrial success In house groups Intel Microsoft Lucent Motorola Commercial model checkers FormalCheck by Cadence Obstacles Scalability is still a problem about 100 state vars Effective use requires great expertise Cache consistency Gigamax Real design of a distributed multiprocessor Global bus UIC UIC M UIC P M P Cluster bus Read shared read owned write invalid write shared Deadlock found using SMV Similar successes IEEE Futurebus standard network RFCs Talk Outline Introduction Foundations q MOCHA q Current Trends and Future Components of a Model Checker q Modeling language Concurrency non determinism simple data types q Requirements language Invariants deadlocks temporal logics q Search algorithms Enumerative vs symbolic many optimizations q Debugging feedback Reachability Problem Model variables X x1 xn Each var is of finite type say boolean Initialization I X condition over X Update T X X How new vars X are related to old vars X as a result of executing one step of the program Target set F X Computational problem Can F be satisfied starting with I by repeatedly applying T Graph Search problem Symbolic Solution Data type region to represent state sets R I X Repeat If R intersects T report yes Else if R contains Post R report no Else R R union Post R Post R X Exists X R X



Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view Model Checking Accomplishments and Opportunities 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 Model Checking Accomplishments and Opportunities 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?