Penn CIS 700 - Survey on Runtime Monitoring based on Formal Specification (65 pages)

Previewing pages 1, 2, 3, 4, 30, 31, 32, 33, 34, 62, 63, 64, 65 of 65 page document View the full content.
View Full Document

Survey on Runtime Monitoring based on Formal Specification



Previewing pages 1, 2, 3, 4, 30, 31, 32, 33, 34, 62, 63, 64, 65 of actual document.

View the full content.
View Full Document
View Full Document

Survey on Runtime Monitoring based on Formal Specification

57 views

Lecture Notes


Pages:
65
School:
University of Pennsylvania
Course:
Cis 700 - Special Topics.
Special Topics. Documents

Unformatted text preview:

Survey on Runtime Monitoring based on Formal Specification WPE II Presentation By Usa Sammapun Oct 28 2005 Software Programs Car ATM Heart Device Aircraft Safe Programs Safe Programs Verification Security Program Development all leg down walk leg2 up leg3 up walk fall leg1 up leg4 up walk fall Model leg1 up leg2 up walk fall walk and not fall Requirement class AIBO Leg leg1 leg2 leg3 leg4 main leg1 new Leg 1 leg2 new Leg 2 leg3 new Leg 3 leg4 new Leg 4 class Leg void walk void stop Implementation Program Safety Techniques Goal Ensuring that implementation satisfies requirement Model Model Checking Model Carrying Code Model Carrying Code Requirement Runtime Monitoring Implementation Outline Overview of runtime monitoring Runtime Verification Security Temporal Assertions using AspectJ Stolz Bodden05 Eagle Barringer et al 04 Edit Automata Bauer et al 03 Eagle for Intrusion Detection Naldurg et al 2004 Discussion Conclusion Runtime Monitoring Formal Specification class AIBO Leg leg1 leg2 leg3 leg4 main leg1 new Leg 1 send checker leg1 leg2 new Leg 2 send checker leg2 leg3 new Leg 3 send checker leg3 leg4 new Leg 4 send checker leg4 class Leg void walk send checker walk void stop send checker stop Programs Satisfied Instrumentation leg1 Trace Extraction leg2 leg3 leg4 Monitor Feedback Not Satisfied Runtime Monitoring Formal specification language Based on Mathematics Instrumentation Manual Automatic Bytecode Sourcecode Specification Evaluation Process Transform spec language into a checking automaton Takes a trace as an input Returns result Satisfied Not Satisfied Direct algorithm Logics Automata Calculi Takes both spec language and a trace as inputs Returns result Satisfied Not Satisfied Feedback Optional Fixed or user defined Outline Overview of runtime monitoring Runtime Verification Security Temporal Assertions using AspectJ Stolz Bodden05 Eagle Barringer et al 04 Edit Automata Bauer et al 03 Eagle for Intrusion Detection Naldurg et al 2004 Comparison and Analysis



View Full Document

Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view Survey on Runtime Monitoring based on Formal Specification 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 Survey on Runtime Monitoring based on Formal Specification 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?