Skip to end of metadata
Go to start of metadata

Meeting Details

  • Moderator: rvh
  • Protocol: sdo
  • Attendees:
    • rvh
    • als
    • ssm
    • lgr
    • nre
    • sdo
    • aas
  • Start: 09:50
  • End: 10:35

Agenda

KEITH presentation (nre)

  • arrows to basic blocks don't work (edges in hierarchy don't work)
  • sliders should not always redraw diagram (for label manager option), to limit the parallel layout requests (Layoutmanager)

Model Checking newXmv (aas)

  • SSA transformation does work now
  • find counter-example is also quick for medium sized models (traffic light)
  • performance of model checker depends on synthesis
  • an example with extended features would be nice (still todo)
  • next steps: test new models and evaluate them (motor example (user input stop, stops everything))
  • SPIN model checker is not as quick as newXmv
  • SPIN uses the synthesized SCG and not SSA form
  • SPIN works for assertions
  • SPIN can not use CTL, only LTL
  • SPIN problem:  One tick in SCCharts does not equal a tick in the spin formula (setting initial values needs a tick): next is not the same. Solved via tickend variable
  • Also needed for newXmv, if the SCG instead of SSA form should be used


  • No labels