scholarly journals Combining specification techniques for processes, data and time

Author(s):  
Ernst-Rüdiger Olderog
Author(s):  
Giles Reger ◽  
David Rydeheard

AbstractParametric runtime verification is the process of verifying properties of execution traces of (data carrying) events produced by a running system. This paper continues our work exploring the relationship between specification techniques for parametric runtime verification. Here we consider the correspondence between trace-slicing automata-based approaches and rule systems. The main contribution is a translation from quantified automata to rule systems, which has been implemented in Scala. This then allows us to highlight the key differences in how the two formalisms handle data, an important step in our wider effort to understand the correspondence between different specification languages for parametric runtime verification. This paper extends a previous conference version of this paper with further examples, a proof of correctness, and an optimisation based on a notion of redundancy observed during the development of the translation.


Author(s):  
Douglas Schenck ◽  
Peter Wilson

Now we turn to the question: ‘Once I have created an abstract declaration in EXPRESS, what would an instance of that thing look like?’ EXPRESS-I allows you to create instances of EXPRESS things that have values in place of references to datatypes. The main reason for doing this is to study some realistic examples of things that otherwise might be difficult to understand. After all, it is one thing to describe a tree and quite another to actually see one. Some of the design goals of EXPRESS-I are based on these requirements: • Major information modeling projects are large and complex. Managing them without appropriate tools based on formal languages and methods is a risky proposition. Informal specification techniques eliminate the possibility of employing computer automation in checking for inconsistencies in presentation or specification. • The language should focus on the display of the realization of the properties of entities, which are the things of interest. The definition of entities is in terms of data and behavior. Data represents the properties by which an entity is realized and behavior is represented by constraints. • The language should seek to avoid, as far as possible, specific implementation views. That is, EXPRESS-I models do not suggest the structure of databases, object bases, or of information bases in general. • The language should provide a means for displaying small populated models of EXPRESS schemas as examples for design reviews. • The language should provide a means for supporting the specification of test suites for information model processors. EXPRESS-I represents entity instances in terms of the values of its attributes (attributes are the traits or characteristics considered important for use and understanding). These values have a representation which might be considered simple (an integer value) or something more complex (an entity value). A geometric point might be defined in terms of three real numbers named x, y and z, and the actual values associated with those attributes might be 1.0, 2.5 and 7.9. The EXPRESS-I instance language provides a means of displaying instantiations of EXPRESS data elements. The language is designed principally for human readability and for ease of generating EXPRESS-I element instances from definitions in an EXPRESS schema.


2020 ◽  
Vol 87 ◽  
pp. 101425 ◽  
Author(s):  
Dominik Bork ◽  
Dimitris Karagiannis ◽  
Benedikt Pittl

Sign in / Sign up

Export Citation Format

Share Document