What we have learnt sofar:

• Angluin L* algorithm for model learning:
  • paper: [1]

  after learning the algorithm we applied it on the A1 machine on page 2 of this slides

• Two main techniques which we studied both to know which, each of us prefer to research on:
  • model checking:
    • slides (Dr. Hojjat University slides): I, II, III
  • model based testing:
    • slides (Dr. Mousavi University slides): I, II –book(for further study): [2]

• Transition Systems and an efficient varient of them called Featured Transition Systems and their model checking algorithm.
  • papers:
    • [3]
      • summary slides: A Summary of Model Checking Lots of Systems Model checking of Featured Transition Systems use sequential product of transition systems. These slides have some examples of this notion which we reviwed in one of the meetings.
      • (main reference for formal definitions) [4]

  As a research problem we were curious whether it is possible to remove priority operator from Featured Transition Systems definition or not. We needed to learn how to write formal and precise proofs. We read [5] about strutured proofs. Here is it’s summary slides.

• Besides Featured Transition Systems as a family-based technique for model checking, we studied FFSMs which is another family-based technique:
  • paper: [6]
    • summary slides: A Summary of: Learning from Difference

• As you may have noticed, model of a particular product changes over time. For example a product might be added a feature to, or it may have a bug fix. One naive approach is that we build a new model from scratch which obviously is not efficient. So we learnt adaptive model learning methods; i.e dynamic model learning and partial dynamic model learning which are more efficient as they initially exploit observation table of the old version.
  • papers:
    • [7]
      • summary slides: A summary of: Learning to reuse
    • [8]
      • summary slides: A summary of : Model Inference and Testing
  • example slides: Dynamic L* example