Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
Model Checking Event-B by Encoding into Alloy
(Extended Abstract)
verfasst von : Paulo J. Matos, João Marques-Silva
Erschienen in: Abstract State Machines, B and Z
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Current day systems are ever more detailed and complex leading to the necessity of developing models that abstract unimportant implementation details while emphasizing their structure. Until recently it was only possible to perform temporal model checking in an
Event
-B model by converting the model to B-METHOD and then using ProB [1]. More recently, a prototype ProB plug in [2] for the RODIN tool has been developed. Nevertheles, encoding
Event
-B to
Alloy
allows building on top of the
Alloy
model finding engine therefore benefiting from all of its optimizations. An extended version of this work is in [3].