Work in progress: Integrating SDL and VDM

Revision as of 21:02, 4 August 2017 by Ttsiodras (talk | contribs) (1 revision imported)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

TASTE-VDM Integration

This section presents some ongoing work in integrating TASTE and VDM See Overture tool to learn about VDM.

The first steps look at SDL-VDM direct integration and simulation.

Summary of the work done so far

ASN.1 Compiler backend: from ASN.1 to VDM Data types

A new backend to the ASN.1 compiler to transform ASN.1 types into native VDM types Input (set of ASN.1 types):

   $ asn1.exe -customStgAstVersion 4 -customStg vdm.stg:dataview.vdm DataView.asn taste-types.asn 


Output in the VDM environment: semantically equivalent data types:


The ASN.1 constraints (ranges) and ASN.1 values were translated to VDM invariants and VDM values.

Link with SDL

A link with SDL and it is now possible to co-simulate a SDL model together with VDM code (with breakpoints in the code, etc).

Example, in the SDL model we declared a procedure and specified it as external. Using a directive we specified that it is implemented in VDM and I give the class name:


At SDL level we can call these two procedures (both have one input and one output params. type FixedIntList is an array of integers:


At first call, "fixed" has value {1,2,3}

The idea is to define the behaviour in SDL and the algos (data manipulation) in VDM - in functional style and strongly typed.

So we created these functions in VDM with compatible types (we should have used the ASN.1-translated types but we did not have them yet in this example):


The first function returns the same list given as input but with each element incremented by one.

On VDM side, we then just run the VDM tool (Overture), which opens a socket waiting for connection, from which you can instantiate VDM objects and call their functions. The parameters are passed using a textual value notation, very similar to the ASN.1 Value Notation. For example a set of elements is passed as "[1,2,3]", a record value is passed as "mk_Typename(field1Value, field2Value, etc.).

So we wrote a parser for the VDM value notation and a translator from ASN.1 (native runtime values) to VDM Value notation.

Now when we run the SDL simulator, it detects the VDM functions (at runtime), connects to the VDM tool and creates an instance of the class where the functions reside:


The GUI appears, and when a send a TC, it makes the call to the two VDM functions and show everything in the MSC (on the fly):


The next steps are to:

  • Automate the generation of VDM function skeletons (easy)
  • Make a case study with more interesting code in VDM
  • Explore the possibility of code generation from VDM (targetting Ada or Rust) - Rust is a language with close semantics/syntax to VDM but with existing LLVM backend.
  • When code generation is there, fully integrate VDM in TASTE