Abstract
This paper primarily reports on semantic aspects of how a formal
specification of the PCTE interfaces has been achieved in a situation
where only a combination of existing formalisms could meet the needs.
The motivations for combining a VDM specification language with a
language of temporal logic, for translating the resulting language,
called VVSL, to an extended COLD-K and for translating it also
(partially) to the language of the logic MPLomega are briefly
outlined.
The main experiences from this work on combination and transformation of
formalisms are presented.
Some important experiences with the application of VVSL to the formal
specification of the PCTE interfaces and otherwise are also mentioned.
Preprint available here.