Using the VDM Tools API

As VDM++ models are executable in VDM Tools, one may wish to interface these models with other applications for a variety of purposes. This brief guide aims to aid a user in developing such an application, using two sample Java source code files.

The code presented was initially developed as part of a proof of concept project "Dynamic Coalitions Workbench" REF TO TR which aimed to allow a domain expert to interact with a model developed in VDM++ without any prior knowledge of the formalism. The project consisted of a VDM model describing information knowledge between agents of a coalition executed in VDM Tools, a driving script and GUI (both developed using Java). The example Java code presented here is a cut down version of that used in the workbench to provide a general mechanism for the interface between VDMTools and Java, and also examples of how to use the interface in a Java application.

Other recommended sources are "Validated Designs for Object-oriented Systems" by John Fitzgerald, Peter Gorm Larsen, Paul Mukherjee, Nico Plat and Marcel Verhoef, and the VDM Toolbox API manual, available here .

Note: When executing the Java application, VDM Tools must be running (the command line version of VDM Tools has a better performance over the graphical version, however the graphical version may help in debugging). Also the VDM API Java package (available in the commercial version of VDMTools) must be in the classpath - it is recommended that the ToolboxAPI.jar file is unpacked (use jar -xvf ToolboxAPI.jar at the command line) and the resultant (jp) folder moved to the classpath.

The VDM++ model runs on the VDMTools interpreter with a VDMController Java object handling all communications between the Java application (in this example an object of the Driver class) and the interpreter. The two supplied Java files are discussed below, with descriptions of the key methods.

VDMController

The VDMController class operates as the interface between VDMTools and the Java application. The key methods shall be outlined here:

init

The init method takes a LinkedList object with the locations of VDM models, creates a new VDM project, adds the models to the project, parses and type checks the files and initialises the interpreter. Note: An exception is thrown in this method see here, the cause of this is unknown, though does not appear to affect the functionality of the link, see here.

evaluateCommand

Evaluates a given command in the interpreter - the expr parameter is the same String that would normally be input into the interpreter (note the keyword "print" is not needed as in VDMTools). No result is given. Note: this method may throw an APIError exception - see the VDMTools API manual for more information.

evaluateExpression

Evaluates a given expression in the interpreter - the expr parameter is the same String that would normally be input into the interpreter (note the keyword "print" is not needed as in VDMTools). A result is returned in the form of a VDMGeneric object. Note: this method may throw an APIError exception - see the VDMTools API manual for more information.

applyOperation

One may wish to use this method for the same purpose as evaluateExpression, where the parameters for the method are the operation in the model and a VDMSequence object. As far as I am aware, there is no real difference between this method and evaluateExpression - we suggest that any developer of a Java application should use whichever method they feel most comfortable with. A result is returned in the form of a VDMGeneric object. Note: this method may throw an APIError exception - see the VDMTools API manual for more information.

Driver

The Driver class acts as the driver of the Java application, with the use of the main method, it may be run from the command line or though the use of an executable jar file. The class initialises the toolbox connection using the VDMController and initiates the Java application. The Driver class proviided has some sample methods to demostrate how a Java application may interact with a VDM model running in VDMTools.

run

This method instantiates a new LinkedList object and adds absolute file name of VDM++ models to the list (the file name must be absolute, as they are passed to VDMTools which is unaware of the relative location of the Java application). This object is passed as a parameter to the init method of the VDMController object. The evaluateCommand method is used to create a new VDM++ object.

sampleCommands

Method to demonstrate how the evaluateCommand method is used. Note that no result is given.

sampleExpression

This method uses the evaluateExpression method to VDMController. A VDMGeneric object is received. This method demonstrates how one may deal with the resultant object, in this example, methods are used to "narrow" the VDMGeneric object into a VDMSet object (the resultant type was known prior to writing the code), the set is iterated through and element removed. There are a variety of such methods available to perform different tasks on different VDM types, see the VDM API guide for more information.

Exception From CORBA Link Creation

When run, the VDMController class throws the followin exception. I have no prior knowledge of CORBA and so the exception does not make sense to me. However, the link still seems to function correctly. If anyone has any ideas as to why this error occurs, please contact me.

22-Jul-2008 11:15:57 com.sun.corba.se.impl.transport.SocketOrChannelConnectionImpl WARNING: "IOP00410201: (COMM_FAILURE) Connection failure: socketType: IIOP_CLEAR_TEXT; hostname: 10.8.150.125; port: 900" org.omg.CORBA.COMM_FAILURE: vmcid: SUN minor code: 201 completed: No at com.sun.corba.se.impl.logging.ORBUtilSystemException.connectFailure(ORBUtilSystemException.java:2172) at com.sun.corba.se.impl.logging.ORBUtilSystemException.connectFailure(ORBUtilSystemException.java:2193) at com.sun.corba.se.impl.transport.SocketOrChannelConnectionImpl.(SocketOrChannelConnectionImpl.java:205) at com.sun.corba.se.impl.transport.SocketOrChannelConnectionImpl.(SocketOrChannelConnectionImpl.java:218) at com.sun.corba.se.impl.transport.SocketOrChannelContactInfoImpl.createConnection(SocketOrChannelContactInfoImpl.java:101) at com.sun.corba.se.impl.protocol.CorbaClientRequestDispatcherImpl.beginRequest(CorbaClientRequestDispatcherImpl.java:152) at com.sun.corba.se.impl.protocol.CorbaClientDelegateImpl.request(CorbaClientDelegateImpl.java:118) at com.sun.corba.se.impl.resolver.BootstrapResolverImpl.invoke(BootstrapResolverImpl.java:74) at com.sun.corba.se.impl.resolver.BootstrapResolverImpl.resolve(BootstrapResolverImpl.java:107) at com.sun.corba.se.impl.resolver.CompositeResolverImpl.resolve(CompositeResolverImpl.java:22) at com.sun.corba.se.impl.resolver.CompositeResolverImpl.resolve(CompositeResolverImpl.java:22) at com.sun.corba.se.impl.resolver.CompositeResolverImpl.resolve(CompositeResolverImpl.java:22) at com.sun.corba.se.impl.orb.ORBImpl.resolve_initial_references(ORBImpl.java:1157) at jp.co.csk.vdm.toolbox.api.ToolboxClient.resolveVDMApplication(ToolboxClient.java:93) at jp.co.csk.vdm.toolbox.api.ToolboxClient.getVDMApplication(ToolboxClient.java:148) at VDMController.init(VDMController.java:35) at Driver.run(Driver.java:48) at Driver.main(Driver.java:29)

Caused by: java.net.ConnectException: Connection refused at sun.nio.ch.Net.connect(Native Method) at sun.nio.ch.SocketChannelImpl.connect(SocketChannelImpl.java:464) at java.nio.channels.SocketChannel.open(SocketChannel.java:146) at com.sun.corba.se.impl.transport.DefaultSocketFactoryImpl.createSocket(DefaultSocketFactoryImpl.java:60) at com.sun.corba.se.impl.transport.SocketOrChannelConnectionImpl.(SocketOrChannelConnectionImpl.java:188) ... 15 more

-- RichardPayne - 22 Jul 2008