Applies formal methods to visual programming
mandated by industry standard. An embedded control system and programmable logic controller industry standard (IEC 1131-3) defines four DSL's that can be represented either diagrammatically or textually utilizing "circuit (i.e. box-and-wire) diagrams, emphasising a data-flow view" and "Petri net diagrams, suited to a control-flow view." (140) The author notes that in general "diagrams are a very natural syntax for software in certain domains; particularly those in which diagrammatic notations form an integral part of design practice and technical discourse" (139) and that
"domain-specific representations of computer software
should accord with, and ideally be derived from existing notations
in the domain." (9) But deriving rigorous conclusions from common diagrammatic manipulation is not trivial:
"While the use of formal methods in supplying evidence is often recommended
or mandated....their practical application remains undeniably difficult...
...many informal or semi-formal arguments are
guided by the structure of some high-level representation of the system,
such as a diagram...the elevation of such arguments to a level admissible
as rigorous evidence requires their formal underpinning, validation and
justification by logical means...
our aim is to apply the theory connecting diagrammatic representations
to semantics in seeking criteria under which representation-driven arguments are
deemed sufficient to provide rigorous evidence without the need of explicitly constructing
fully formal proofs. (144)"
Posted to DSL by jon fernquest on 8/2/02; 11:48:30 PM