New User Special Price Expires in

Let's log you in.

Sign in with Facebook


Don't have a StudySoup account? Create one here!


Create a StudySoup account

Be part of our community, it's free to join!

Sign up with Facebook


Create your account
By creating an account you agree to StudySoup's terms and conditions and privacy policy

Already have a StudySoup account? Login here


by: Ryley Lang


Ryley Lang
GPA 3.8


Almost Ready


These notes were just uploaded, and will be ready to view shortly.

Purchase these notes here, or revisit this page.

Either way, we'll remind you when they're ready :)

Preview These Notes for FREE

Get a free preview of these Notes, just enter your email below.

Unlock Preview
Unlock Preview

Preview these materials now for free

Why put in your email? Get access to more of this material and other relevant free materials for your school

View Preview

About this Document

Class Notes
25 ?




Popular in Course

Popular in ComputerScienence

This 29 page Class Notes was uploaded by Ryley Lang on Sunday September 6, 2015. The Class Notes belongs to C S 378 at University of Texas at Austin taught by Staff in Fall. Since its upload, it has received 33 views. For similar materials see /class/181672/c-s-378-university-of-texas-at-austin in ComputerScienence at University of Texas at Austin.

Popular in ComputerScienence




Report this Material


What is Karma?


Karma is the currency of StudySoup.

You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!

Date Created: 09/06/15
Template for Unification of Verification and Validation Static Analysis Property Specifications Environment Specifications Symbolic Execution Abstraction and Translation Model Checking Composition Architecture Specifications I Verified Components I 1 Runtime Monitors Theorem Proving 922008 Design For Verification Design For Verification Design Goals Functionality Robustness Peformance Security Verifiability Design for verifiability is required for the other goals to be meaningful Verification has no hope for success unless the program is designed with verification as a goal We need a design process leading to verifiable systems 922008 Design For Verification What Makes a System Difficult to Verify Complexity of structure Size of units to be verified Nonlocal state Obscure specification of state Distribution of functionality across multiple units 922008 Design For Verification What Design Characteristics Make a System Verifiable Precisely Specified Structure Separation of functional concerns Localized state Verifiable components 922008 Design For Verification 922008 Systems and Architectures 0 Components Interactions System Environment Design For Verification 5 Foundations for Verifiable Design Formal architectural specification for system Components and relationships among components System level properties and environment requirements Formal specification of components Properties and environments Executable 922008 Design For Verification Role of Architectures Structure and Behavior of System Enables formal definition of environments and requirements Enables derivation of components and their relationships Enables derivation of component properties and environments 922008 Design For Verification Role of Components 1 Components provide a semantic basis for de nition of properties and assumptions 2 Properties can be established on components under assumptions Wthh model composnions and execution env1ronments 3 The components can then be replaced in veri cations of compositions by an adequate set of established properties 4 Exhaustive analysis andor testin is sometimes possible on a component by component a51s 5 Components provide a basis for larger semantic units for monltorlng and de nition of redundancy 6 Patterns of com onents enable de nition of properties to be de ned an assumptions for veri cation of properties 922008 Design For Verification Properties and Environments Properties are statements about the Property states of the program Actually Specifications state machines themselves V Design Methodology ComponentProgram ErWironment The environment is a state machine Specifications which generates inputs and accepts outputs from the program 922008 Design For Verification DesignDevelopment Flow Environ ent Req irements Archi cture Sp cification Compo ents Relationships Component Specific ion fEnviKmentsProperties Component Verification Component Composition Pro ram 922008 Design For Verification 1O Qeww 922008 Architecture Definition Architectures An architecture composes components through relationships to implement an inputoutput specification which conforms to a set of properties required by its environment with internal behavior defined by an execution model An architecture is often defined in terms of layers of functionalityabstraction There are architectures templates or patterns associated with each level of abstraction Each layerlevel has a set of components An instance of the architecture is defined by a choice of execution environment and initialization Components are either selected from libraries or developed for a specific application Design For Verification 11 Components Definition A component provides one or more logical functions at the level of abstraction at which it is defined A component is a functional specification an interface a set of properties and an implementation The properties are determined by the functional specification and the architecture which defines the component environment The properties necessary to guarantee the functional specifications used in the architecture are determined by the component environment Components may defined within an architecture or generic components which are adapted for an architecture 922008 Design For Verification 12 6 7 922008 machines Components Design Design and development begins with writing functional specifications and deriving properties for the component from the functional specifications The control flow of a component is defined by a state machine The actions associated with each state Moore or transition Mealy must be run to completion The states in the properties of the component must be explicitly visible in the componentprogram design Transitions among states in the property specifications should be explicitly visible in the componentprogram design Data which is shared among a set of components should be encapsulated in a separate component The input and output sequences environment for a component should be specifiable as a state machineor set of state Design For Verification 13 RelationshipsConnectorslnteractions Definition Connector is a word often used in the software architecture literature to denote the relationship among components in an architecture Interactions is my preferred word since they may be implicit Interactions may be defined explicitly in a language or implicitly through matching of component specifications An interaction is an execution of a connectorrelationship Examples Procedure invocations Continuations data flow Callbacks 922008 Design For Verification 14 J gunm u 3mm m Mgm r1 Iagq m WW m mu mum mum 2 um w m mum Mm mm w W nmkwxm mgmv 3 mm In mm mam Wm 3 59 magma mm a um mu m M1351 Mm mm WILRIHSJQ 14113 Fm up rm mun I m 1 m 17hr m n chumum D a klivmh39 mm 9 tam UM L1 l ax mm mum matte w am maLmzw Mymw u r m mm gm Architectural Derivation Specify the environment in which the system will be defined The specification may be in terms of message sequence charts state machines or temporal logic properties Specify the required properties for the system in an appropriate logic or as a set of state machines Specify layers of abstraction within which components may be defined There may be only a single layer Specify components within each layer Specify the relationships interactions or connectors within each layer and across layers as event streams dependence graphs andor callreturn invocations including sequencing of interactions in the relationship Steps 2 3 4 and 5 define a classical software architecture Derive those properties of components which are required as a result of system properties and the relationships among components 922008 Design For Verification 18 Component Specification and Verification Environment FA be l 1 E X ll Modules may require context information to satisfy a property Assumption Module gt Property assumeguarantee reasoning How are assumptions obtained Developer encodes them Abstractions of environment if known Automatically generate exact assumption A 922008 Design For Verification 19 Component Specification and Verification 1 Identify the sources of components in libraries andor as application specific 2 The properties of a component are the union of the properties derived with the functionality of the component and the requirements imposed by the architecture 3 Verify the properties of the primitive components using the architecture to derive the environment of the primitive components 922008 Design For Verification 20 Component Composition Phase Overview 1 Use the architecture to determine pairs or sets of components which can or should be composed into components visible in the architecture 2 Follow the procedure given following to compose components into larger components Verify properties with respect to environment derived from architecture 3 Compose components at lower levels of abstraction following architecture and conformance of properties to get components at higher levels of abstraction 922008 Design For Verification 21 Component Composition Phase 1 N 922008 Determine consistency between the environments used for component property verification and the environment generated by the architecture Replace components by verified properties Determine the properties and environment of the composed component Verify the properties of composed component by appropriate methods Continue steps 1 and 4 until architecture is realized and system properties established Design For Verification 22 Comments Architectures may be designed from scratch or be examples of patterns Architectures are nearly always implemented with a mixture of library and application specific components Incorporation of components from libraries requires special consideration since specifications source and properties may not be available 922008 Design For Verification 23 Example Simple Microwave Oven Microwave Oven Speci cation This simple oven has a single control button When the oven door is closed and the user presses the button the oven will cook that is energize the power tube for 1 minute There is a light inside the oven Any time the oven is cooking the light must be turned on so you can peer through the window in the oven39s door and see if your food is bubbling Any time the door is open the light must be on so you can see your food or so you have enough light to clean the oven When the oven times out cooks until the desired preset time it turns off both the power tube and the light It then emits a warning beep to signal that the food is ready The user can stop the cooking by opening the door Once the door is opened the timer resets to zero Closing the oven door turns out the light 922008 Design For Verification 24 Properties If the door is open the tube is not on or If the Door is open then the Tube is off If the button is pushed while the Door is closed the Light and the Tube will turn on If the Door is open then the Light is on If the Light is on then the Door is open or the Tube is on 922008 Design For Verification 25 State Table for Microwave Oven 7 buttonFr sseci daor pened duelClosed l timerTimesDut Ready Te Coolc Cauling Door Open 2 v Caching Looking Lookini Ctrakin i d g Extended i ntE rrupted 5 Le T39iDlEIE Cooking i quota k L 5007C en template Lquot Q 1N3 39p l kag i ReadvTe COM 3 interruptece 39 Deer Open 39 Ready I i cranking Cooking cooking coercing Extended Extended interrupted i Compiete i 922008 Design For Verification 26 State Table for Microwave Oven bu un Fressed damOpened l dourclesed timerTimes ut Ready Te Clank Cracking Door Open C an39f Happen Event ignored aking r Ecolting Cracking Exsended intermm d Can Happen hooking Complete cooking Conk n Demo er Can39t Ha ened Can39rHa in Complete I g p I 39 pp 39 pPE anking Eve tl ed C I Hi an Head 39To C r Event med Interrupted n gnor a pp quot y 00 9 Dear Open Event ignm39eci Can t Happen Ready To Cook 031139 Happen Caching Cooking 39 39 39 C I t Extended cranking Extended mlenupted an Happen ranking Camp 9 6 Design For Verification 27 922008 Components Door open closed Power tube on offwattage etc Light on off wattage etc Timer on and counting down off and zero Beeper on off Button Event generator 922008 Design For Verification 28


Buy Material

Are you sure you want to buy this material for

25 Karma

Buy Material

BOOM! Enjoy Your Free Notes!

We've added these Notes to your profile, click here to view them now.


You're already Subscribed!

Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'

Why people love StudySoup

Bentley McCaw University of Florida

"I was shooting for a perfect 4.0 GPA this semester. Having StudySoup as a study aid was critical to helping me achieve my goal...and I nailed it!"

Janice Dongeun University of Washington

"I used the money I made selling my notes & study guides to pay for spring break in Olympia, Washington...which was Sweet!"

Steve Martinelli UC Los Angeles

"There's no way I would have passed my Organic Chemistry class this semester without the notes and study guides I got from StudySoup."

Parker Thompson 500 Startups

"It's a great way for students to improve their educational experience and it seemed like a product that everybody wants, so all the people participating are winning."

Become an Elite Notetaker and start selling your notes online!

Refund Policy


All subscriptions to StudySoup are paid in full at the time of subscribing. To change your credit card information or to cancel your subscription, go to "Edit Settings". All credit card information will be available there. If you should decide to cancel your subscription, it will continue to be valid until the next payment period, as all payments for the current period were made in advance. For special circumstances, please email


StudySoup has more than 1 million course-specific study resources to help students study smarter. If you’re having trouble finding what you’re looking for, our customer support team can help you find what you need! Feel free to contact them here:

Recurring Subscriptions: If you have canceled your recurring subscription on the day of renewal and have not downloaded any documents, you may request a refund by submitting an email to

Satisfaction Guarantee: If you’re not satisfied with your subscription, you can contact us for further help. Contact must be made within 3 business days of your subscription purchase and your refund request will be subject for review.

Please Note: Refunds can never be provided more than 30 days after the initial purchase date regardless of your activity on the site.