administrivia

3792 users shared this document! click

Formal Methods CS208-18 1 administrivia quiz results somewhat disappointing overall
many people did well
some people ...
mean 82, median 86 today start formal methods
some time at end of class for group coordination
prepare for Thursday Formal Methods CS208-18 2 project 2 written deliverables due Thursday system design
ui design use the examples in the notes for guidance I am looking for something similar out of you you may submit rough code design to get feedback Formal Methods CS208-18 3 project Thursday presentations 20-25 minutes per group on Thursday describe high level view of complete sys design
can describe UI
can go into detail on interesting aspect of design any questions about Thursday? or project in general? Formal Methods CS208-18 4 code design when finalizing code design, need to choose target language officially language agnostic for this course previously, more success in java than C++ even if group did not know java up front your choice grade depends on accomplishment
not language choice Formal Methods CS208-18 5 formal methods using formal (precise, mathematical) notations to describe and reason about software traditional formal methods expensive justifiable for life-critical only
not feasible for most projects light weight formal methods being developed
more justifiable Formal Methods CS208-18 6 formal approach need 2 formal descriptions system
goal system specification design
code goal can be from requirements
can be from design Formal Methods CS208-18 7 formal outcome can prove goals from system
can find counterexamples
proving goal is traditional target
provides greater assurance finding counterexamples easier
provides guidance on what to fix
much more broadly justifiable Formal Methods CS208-18 8 current tools tools available to help automated tools for proving called theorem provers
very people expensive search for counterexamples model checkers and relational checkers
cheap to use Formal Methods CS208-18 9 preview consider 2 dimensions design vs code — next semester
proving vs model checking four total possibilities only look at model checking design this semester will examine 3 notations for designs Z/ladybug
temporal logic/SMV
CSP/fdr Formal Methods CS208-18 10 formal notations discussing 3 formal design notations Z/np focus on structural properties
temporal logic focus on simple dynamic
csp focus on multiple process dynamics want you need understand what each can do
why bother with formal methods don’t need to be able to write specs Formal Methods CS208-18 11 Z today talk about Z (and np)
Z most widely used formal notation
still miniscule usage
developed at Oxford focuses on structural issues can this structure have a cycle?
is this field unique? Formal Methods CS208-18 12 nitpick/ladybug three tools to check Z-like specs nitpick written by Jackson (MIT) and me
ladybug written by me
alloy written by Jackson nitpick, ladybug use np language almost subset of Z
first-order (more on this later) about to not be true uses ascii only Formal Methods CS208-18 13 UML example Order dateReceived isPrepaid number Price dispatch() close() Customer name address creditRating() Corporate Customer companyName creditRating creditLimit remind() creditCard# Personal Customer Employee OrderLine quantity price isSatisfied Product 1 line
items * 1 * sales rep 0..1 1 * * Formal Methods CS208-18 14 np types 3 kinds of things in np scalar objects (think enum)
sets of scalar objects
relations over scalar objects schemas provide structuring name = [ declarations | constraints ] almost class-like | constraints is optional Formal Methods CS208-18 15 np types np model instances represented by scalar objects
types are sets of instances top level types declared specially [Order,Customer,OrderLine,Product,Employee] enumerated types declared specially Rating == { poor, … } subtypes declared as subsets OrderSystem = [
CorporateCustomer : set Customer
PersonalCustomer : set Customer Formal Methods CS208-18 16 associations/attributes associations and attributes usually given as functions
from class defining attribute
to class/type of attribute or association simple multiplicity represented with total vs. partial, functional, injective creditRating : tot Customer -> Rating
customerOrder : tot Order -> Customer
orderLines : tot OrderLine -> Order
product : tot OrderLine -> Product
salesRep : CorporateCustomer -> Employee Formal Methods CS208-18 17 other attributes boolean fields modeled as sets set of type defining field
inclusion means attribute is true
exclusion means attribute is false
{ x : Class | x.field == true} isPrepaid : set Order many attributes abstracted away Formal Methods CS208-18 18 declarations declaration parts define structure akin to what UML class diagram shows describe attributes/associations over groups of instances a la classes
“backwards” descriptions describe the entire relationship at once
OO takes viewpoint of single instance at time important distinction different way of thinking
some things become easier to describe Formal Methods CS208-18 19 constraints constraints limit allowable cases akin to OCL constraints included in constraints section name = [ declarations | constraints ] Formal Methods CS208-18 20 relational expressions constraints are relational expressions operate on scalars, sets and relations traditional operations (some odd notation)
U & / union, intersection, difference
~ + inverse, transitive closure
* reflexive transitive closure
dom ran actual domain, range
= <= < equality, subset, proper subset and not or => <=> Formal Methods CS208-18 21 more operators domain restriction s <| r
all pairs in r with first element in s also range restriction
also negative domain, range restriction f.o function application
r.{s} relational image fun, tot, inj, bij is relation functional, total, injective, bijective Formal Methods CS208-18 22 examples CorporateCustomer & PersonalCustomer = {} ran (PersonalCustomer <| creditRating) =
{ poor} Formal Methods CS208-18 23 properties schemas can be used to describe collections of states referred to as properties
describe desirable or undesirable states include other schemas in declarations grants visibility to all its state Safe =
[
OrderSystem
|
customerOrder~.{creditRating~.{poor}} <=
isPrepaid
] Formal Methods CS208-18 24 operations only described static structure so far every interesting system changes operation is special kind of schema add parameter list to schema name may be empty
parameter values are constant during op
other variables have pre and post values
post-state is primed Formal Methods CS208-18 25 operation example addOrder(o:Order, ol:OrderLine) =
[
OrderSystem
| orderLines ' .ol = o orderLines < orderLines ' dom orderLines U { ol } =
dom orderLines ' ] Formal Methods CS208-18 26 claims claims are the goals replace = with :: in any schema isSafe(o:Order, c:Customer)::
[
OrderSystem
| Safe and addOrder(o,c) => Safe ' ] Formal Methods CS208-18 27 common claims two common categories of claims invariance property and operation => property ' implication property => property2 Formal Methods CS208-18 28 checking ladybug will check that claim holds for all possible instantiations limited by scope number of instances of each type
limited to small numbers (5±) ladybug returns counterexamples if any
limited to roughly 10120 total states
usually finishes in seconds Formal Methods CS208-18 29 example consider memory allocator (malloc)
model in terms of functions, sets key concepts in allocator usage maps addresses to data used set of addresses in use newAddr new address allocated Formal Methods CS208-18 30 allocator example Addr Data usage maps addresses to data used includes addresses in use Formal Methods CS208-18 31 allocator example Addr Data usage’ maps addresses to data used’ includes addresses in use newAddr is the newly allocated address Formal Methods CS208-18 32 formalizing allocator model imposes restrictions
addresses in use map data used = dom usage
used’ = dom usage’ allocation does not change mapping of existing memory used r usage’ = usage Formal Methods CS208-18 33 formalizing allocator
newly allocated address now in use used’ = used U { newAddr } goal: newAddress not already in use not newAddr e used Formal Methods CS208-18 34 target formula convert claim to single formula
system and not goal for allocator used = dom usage and used’ = dom usage’ and used r usage’ = usage and
used’ = used U { newAddr } and
newAddr e used Formal Methods CS208-18 35 counterexamples in less than one second: Found Counterexample to Claim uniqueAddrAlloc:
a : Addr =
a0 inUse : set Addr =
{ a0 } inUse' : set Addr =
{ a0 } usage : Addr->Value =
{ a0 -> v0 } usage' : Addr->Value =
{ a0 -> v0 } Found 1 Counterexample Formal Methods CS208-18 36 experiences ladybug still research tool has several success stories found mobile ipv6 bug
found bug in proof of faa system safety
found bugs in HLA
used to check british rail system spec Formal Methods CS208-18 37 allocator specification (1) /* A trivial specification of a memory allocator - e.g. malloc */ /* Specify the given types */ [Addr, Data] /* Define the heap itself with a schema */ Heap =
[ /* Define Variables */ usage : Addr -> Data
used : set Addr= | /* all currently mapped addresses are used*/ used = dom usage ] Formal Methods CS208-18 38 allocator specification (2) /* Alloc: an operation to allocate memory */ Alloc(newAddr : Addr) = /* newAddr is the newly alloc’d addr */ [ Heap /* Include the Heap definition */ |
/* The existing part of usage' is unchanged*/ used <: usage' = usage /* newAddr is now mapped(to unspecified data) */ used' = used U {newAddr} ] Formal Methods CS208-18 39 allocator specification (3) /* Make a claim about Alloc */ uniqueAddrAlloc::
[
Heap newAddr : Addr |
/* A newly allocated addr should not have been in use */ Alloc(newAddr) => newAddr not in use ]

Comments