Innehållsförteckning
Development of Formally Verified Erlang Programs a case study
Research question
AXD 301 Architecture
AXD 301 Architecture
PPT-bild
PPT-bild
PPT-bild
Application lock
PPT-bild
example
example
Supervisor processes
Testing versus Verification
Mutual exclusion (at most one client has access to resource)
testing
Verification: generate State Space
Erlang -> transitions
Erlang -> transitions
Erlang -> transitions
Erlang -> transitions
State Space analysis
State Space analysis
Conclusions
|