Meeduse

Meeduse allows to mix the formal B Method with Domain Specific Languages designed in the Eclipse Modeling Framework (EMF)

More information about the tool can be found at: http://vasco.imag.fr/tools/meeduse/

1. The GPU scheduler

1.1. Static semantics

The XText Grammar

The meta-model

Formal model

The functional B specification of the meta-model: [pdf]

1.2. Dynamic semantics

The meta-model based approach

• Abstract specification: [pdf]
• Concrete specification: [pdf]

The CP-net approach

• Formal specification: [pdf]