Upgrade to Pro — share decks privately, control downloads, hide ads and more …

Autofunk: An Inference-Based Formal Model Gener...

Autofunk: An Inference-Based Formal Model Generation Framework for Production Systems (FM 2015)

In this paper, we present Autofunk, a fast and scalable framework designed at Michelin to automatically build formal models (Symbolic Transition Systems) based on production messages gathered from production systems themselves. Our approach combines model-driven engineering with rule-based expert systems and human knowledge.

Online slides: http://slides.williamdurand.fr/fm2015/
Sources: https://github.com/willdurand-slides/fm2015

William Durand

June 25, 2015
Tweet

More Decks by William Durand

Other Decks in Research

Transcript

  1. Autofunk: an Inference-Based Formal Model Generation Framework for [Michelin] Production

    Systems. William Durand, Sébastien Salva — June 25, 2015 / FM'15
  2. A production system is composed of devices, production machines, and

    one or more software to control them.  In our case, we target a single workshop only.
  3. Software exchange information with points and machines by sending and

    receiving production messages. 1 7 - J u n - 2 0 1 5 2 3 : 2 9 : 5 9 . 5 0 | 1 7 0 1 1 | M S G _ I N [ p i d : 1 ] [ n s e c : 8 ] [ p o i n t : 1 ] . . . 1 7 - J u n - 2 0 1 5 2 3 : 2 9 : 5 9 . 6 1 | 1 7 0 2 1 | M S G _ O U T [ p i d : 1 ] [ n s e c : 8 ] [ p o i n t : 3 ] . . . 1 7 - J u n - 2 0 1 5 2 3 : 2 9 : 5 9 . 7 0 | 1 7 0 1 1 | M S G _ I N [ p i d : 2 ] [ n s e c : 8 ] [ p o i n t : 2 ] . . .
  4. Each production message is tied to a product (e.g. tire),

    identified by a product identifier (p i d ). Gathering all production messages related to a product allows to retrieve what happened to it.
  5. Developement Teams POV 100+ applications running in production Not (fully)

    covered by tests Documentation most likely outdated MUST be maintained for ~20 years!
  6. Customers (Factories) POV Stability over anything else Maintenance periods are

    planned, but rather long (> 1 week) 1h (unexpected) downtime = 50k $
  7. Testing such production systems is complex, and takes a lot

    of time as it implies the physical devices, and there are numerous behaviours.
  8. These behaviours could be formally described into a model. But

    writing such models is an heavy task and error prone.  Not suitable for Michelin applications.
  9. Our Approach By leveraging the information found in the production

    messages, we build formal and exact models (STS) that describe functional behaviours of a production system under analysis.
  10. Autofunk Combines different fields: model inference, expert systems, and (now)

    machine learning Written in Java 8, reusing powerful libraries (e.g. , ) More a Proof of Concept than a production- ready tool To be open sourced (no ETA yet) Spark Drools
  11. Experimentation 10 million production messages (20 days)  161,035 traces

     S R ( S ) 77,058 branches 1,587 branches 43,536 branches 1,585 branches  2 entry points here It took 5 minutes to build the two models.
  12. Offline Passive Testing Inferred models are used as specifications Another

    set of traces is collected on a system under test S U T (new or upgraded)  Does S U T conforms to the specifications?
  13. Conclusion Fast and efficient technique to infer formal models The

    more production messages, the better! But a few technical issues to tackle (memory consumption for instance)
  14. Future Work Deploying Autofunk as a real solution (WIP) Offline

    passive testing (WIP) Online passive testing