Formal Verification of Distributed Systems in EECS498

eecs498 eecs498 008 formal verification of formal n.w
1 / 19
Embed
Share

Dive into the world of formal verification with EECS498-008 course material created by Jon Howell and Manos Kapritsos. Explore the concepts of distributed systems, trusted vs proven systems, and the systems specification sandwich. Get insights into host communication, network behavior, file system operations, and more. Stay updated on course deadlines and announcements for a successful academic journey in EECS498.

  • EECS498
  • Formal Verification
  • Distributed Systems
  • Trusted Systems
  • Meta Description
rayaanacharya
gloc Follow

Uploaded on | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.

Download Presentation

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.

E N D

Presentation Transcript

  1. EECS498 EECS498- -008 Formal Verification of Formal Verification of Systems Software Systems Software 008 Material and slides created by Jon Howell and Manos Kapritsos

  2. A distributed system is composed of multiple hosts, a network and clocks Distributed system: attempt #3 module DistributedSystem { datatype Variables = Variables(hosts:seq<Host.Variables>, network: Network.Variables, Distributed system time: Time.Variables) Host Host predicate Next(v, v , hostid, msgOps: MessageOps, clk:Time) { Network || (&& HostAction(v, v , hostid, msgOps) && Network.Next(v, v , msgOps) Time && Time.Read(v.time, clk)) Host Host || (&& Time.Advance(v.time, v .time) && v .hosts == v.hosts && v .network == v.network) } } 3/21/2025 EECS498-008 2

  3. A distributed system module DistributedSystem { datatype Variables = Variables(fs: FileSystem.Variables, disk: Disk.Variables) Distributed system predicate Next(v, v ) { || (exists io :: && FileSystem.Next(v.fs, v .fs, io) Binding variable File system (in-memory state && Disk.Next(v.disk, v .disk, io) Disk || ( // Crash! && FileSystem.Init(v .fs) && v .disk == v.disk ) } } 3/21/2025 EECS498-008 3

  4. Trusted vs proven Trusted vs proven Hosts cannot communicate except through the network Time can advance between any host steps File system (kernel) can crash Distributed system Distributed system Disk won t forget writes it acknowledged Network won t make up packets Host Host Network File system (in-memory state Disk Network might reorder packets Time Host Host Disk might reorder concurrent writes Time only moves forward 3/21/2025 EECS498-008 4

  5. : the systems specification sandwich : the systems specification sandwich trusted application spec proof protocol proof code trusted environment assumptions image: pixabay 3/21/2025 EECS498-008 5

  6. Administrivia Administrivia Midterm went great, congratulations! Problem set 3 due on Friday Project 1 will be released on Monday Let me know if you can t find teammates Midterm evaluations due today! They are really, really important If we reach 66%, I ll design custom course stickers I m giving another lecture right after this one, so I have to skip IOH 3/21/2025 EECS498-008 6

  7. Chapter 6: Refinement Chapter 6: Refinement 3/21/2025 EECS498-008 7

  8. State machines: a versatile tool State machines: a versatile tool State machines can be used to Model the program Model environment components Model how the system (program+environment) fits together Specify the system behavior 3/21/2025 EECS498-008 8

  9. Different ways to specify behavior Different ways to specify behavior Spec C-style assertions Postconditions Properties/invariants Distributed system Refinement to a state machine Host Network Host Host 3/21/2025 EECS498-008 9

  10. Example: Example: hashtable hashtable module HashTable { datatype Variables = Variables(tbl:seq<Pair<int, string>>) predicate Insert(v:Variables, v :Variables, key:int, val:string) { var free := Probe(v.tbl, key); && free.Some? && v .tbl == v.tbl[free.value := Pair(key, val)] } } - - - 13 C 13 C - - - - - - 23 A 23 A 23 A 23 A - - - - 47 D - - 71 B 71 B 71 B 10

  11. The spec: a simple map The spec: a simple map 13 C 23 A 47 D 71 B 13 C 23 A 71 B 23 A 71 B (empty) 23 A module MapSpec { datatype Variables = Variables(mapp:map<Key, Value>) predicate InsertOp(v:Variables, v':Variables, key:Key, value:Value) { && v'.mapp == v.mapp[key := value] } } 11

  12. Refinement Refinement 13 C 23 A 47 D 71 B 13 C 23 A 71 B 23 A 71 B (empty) 23 A - - - 13 C 13 C - - - - - - 23 A 23 A 23 A 23 A - - - - 47 D - - 71 B 71 B 71 B 12

  13. The benefits of refinement The benefits of refinement Refinement allows for good specs Abstract: elide implementation details Concise: simple state machine Complete: better than a bag of properties But if you want, you can prove properties about the spec Refinement is very powerful Can specify systems that are hard to specify otherwise E.g. linearizability 3/21/2025 EECS498-008 13

  14. A A sharded sharded key key- -value store value store Logically centralized, physically distributed 13 C 23 A 47 D 71 B 13 C 23 A 71 B 23 A 71 B (empty) 23 A Host 1 Host 1 - Host 1 13 C Host 1 13 C Host 1 - - - - - - - - - - - - Host 2 Host 2 Host 2 Host 2 Host 2 23 A 23 A 23 A - 23 A - - 47 D - - - 71 B 71 B - 71 B 14

  15. Stutter steps Stutter steps One stutter step for the spec 23 A 71 B 23 A 71 B (empty) 23 A Host 1 - Host 1 23 A Host 1 Host 1 - - - - - - One normal step for the implementation - - - - Host 2 Host 2 Host 2 Host 2 23 A - 23 A - - - - - - 71 B 71 B - 15

  16. A primary A primary- -backup protocol backup protocol Clients Primary Primary Backup Backup 16

  17. A primary A primary- -backup protocol backup protocol Primary Primary Primary Primary Primary Primary Backup Backup Backup Backup Backup Backup 17

  18. The The interpretation (Abstraction interpretation (Abstraction) function ) function 13 C 23 A 47 D 71 B 13 C 23 A 71 B 23 A 71 B (empty) 23 A function Abstraction(lv:HashTblState) : (hv:MapSpec.Variables) { ... } - - - 13 C 13 C - - - - - - 23 A 23 A 23 A 23 A - - - - 47 D - - 71 B 71 B 71 B 18

  19. A refinement proof A refinement proof function Abstraction(v:Variables) : MapSpec.Variables predicate Inv(v:Variables) lemma RefinementInit(v:Variables) requires Init(v) ensures Inv(v) // Inv base case ensures MapSpec.Init(Abstraction(v)) // Refinement base case lemma RefinementNext(v:Variables, v':Variables) requires Next(v, v') requires Inv(v) ensures Inv(v') // Inv inductive step ensures MapSpec.Next(Abstraction(v), Abstraction(v')) // Refinement inductive step || Abstraction(v) == Abstraction(v') // OR stutter step 19

Related


No related presentations.

More Related Content