Rev 46 | Blame | Compare with Previous | Last modification | View Log | RSS feed

% aims

% * support for agreements in project planning:

% * What is the TPPL prototype good for ?

% * What are general directions of development for successors ?

% * Reflect possibly different views of TP, software verification and CA

% * raw material for proposal

\documentclass[11pt,a4paper]{scrartcl}

\usepackage{ucs}

\usepackage[utf8x]{inputenc}

\usepackage[onehalfspacing]{setspace}

\usepackage{paralist}

\usepackage{url}

\bibliographystyle{alpha}

\usepackage{graphicx}

\usepackage{sty/editing} %DISABLE FOR FINAL VERSION

\title{Design and Prototype for a \\

TP-based Programming Language\\

{\Large Draft for an FWF proposal}}

\begin{document}

\begin{spacing}{1}

\tableofcontents

\bigskip \bigskip

\section{Theorem Proving underway to Engineering Practice}

% This section picks out the note ``that the aim of this project is to

% provide a running prototype environment'' in \S\ref{mission} and goes

% beyond the mission stated there.

Interdisciplinary work as addressed in the proposal ``Design and

Prototype for a TP-based Programming Language (TP-PL)'' is best begun

by sharing visions between TP-PL developers and potential users. Such

visions shall be a fertile soil for joint work to identify applications

of TP-PL, which create a win-win situation for users and developers.

These notes shall

serve this purpose and start from a wider perspective going beyond the

proposal text.

\subsection{Engineers' attitudes towards mathematical software}

In applied sciences there are strong attitudes towards usage of

mathematical software which in turn are a constituent part of

professional values and ethics.

A first aspect of the attitudes reflects a great success of computer

mathematics, in numeric as well as in symbolic computation: Engineers

and experts in applied sciences have high expectations with regard to

computational power of tools like Mathematica, Mathlab or Maple, for

instance when solving huge equational systems, when performing

enormous numbers of computations or when simplifying large terms.

A second aspect of the attitudes addresses deficiencies of

mathematical software still considered inevitable: Engineers are

taught to be personally responsible for results of mathematical

software and to be always alert for casual inappropriate results due

to ill-conditioned systems, e.g.~numerical instabilities with floating

point numbers or issues related to multivalued functions

\cite{davenport-10:multivalued}~\footnote{Errors cited from

\cite{hoelzl09realineequalities}

are $\int^1_{-1}{\sqrt{x^2}dx}=0$ instead of $=1$ (Maple, \url{http://www.maplesoft.com/products/Maple/}) and

$\int^1_{-1}{\frac{1}{\sqrt{x^2}}dx}=0$ instead of ``undefined''

(Mathematica, \url{http://www.wolfram.com/mathematica/}).}.

\medskip So these traditional attitudes and expectations have good

reasons and must be taken into account when TP is approaching

engineering practice.

\subsection{Computer Mathematics' approaches to engineering practice}

There are several success stories of rigorous formal approaches to

engineering problems with impact on practice.

TP is particularly successful in software verification \footnote{A representative

overview can be gained from the publication lists of the Verisoft project

at \url{http://www.verisoft.de/PublikationSeite.html}},

but has also gained revenue in mechanised proofs for sizable mathematical

problems, e.g.~the Kepler Conjecture\footnote{\url{http://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet}}

or the Four Colour Theorem \cite{DBLP:conf/ascm/Gonthier07}.

Success stories of certified and verified Computer Algebra are

\cite{TODO-verified-CA}.

\footnote{fixme[Further success stories of CA?]}

\bigskip Apart from the approaches by the dedicated academic

communities from TP and from CA respectively there are further

approaches with similar goals. One integrative approach from the side of computer

science is called ``Formal Methods

(FM)''~\cite{fm-03}~\footnote{http://www.fmeurope.org/}, an approach

which actually has been born in Austria and which is still alive as

``Vienna Development Method

(VDM)''~\cite{vdm-09}~\footnote{http://www.vdmportal.org/twiki/bin/view}.

This community promotes several successful projects, for instance the

COMPASS project~\footnote{www.compass-research.eu} with the goal of

supporting the engineering of dependable systems-of-systems based on

contractual styles of interface specification. Proof support is under

development and ``is expected to build on HOL''~\fixme[Which HOL? Reference imprecise.]~\footnote{Deliverable

D33.2 ``Theorem Proving Support'' at

http://www.compass-research.eu/deliverables.html.}. These goals are

close to those of the TP-PL project such that the proposal has to

refer to such projects.

\medskip Another approach from the side of applied mathematics is

called ``Systems Modeling (SM)'' split into various directions from

Operational Research to such specific technologies like

``Vehicle Systems Model-ling and

Testing''~\footnote{http://www.inderscience.com/jhome.php?jcode=ijvsmt}.

These approaches build on graphical representations of problems and

solutions rather than on representation based on formal logic. From

this side come easy-to-adopt mathematical tools like Maple's

MapleSim~\footnote{http://www.maplesoft.com/products/maplesim} and

Mathematica's System

Modeler~\footnote{http://www.wolfram.com/system-modeler}.

\subsection{What are the promises of TP + CA?}

A generally promising aspect of the TP-PL proposal is that explicit

cooperation is established between two institutes, Theorem Proving

Group at TUM and Research Institute for Symbolic Computation at JKU,

each leading in the respective domain: The former develops Isabelle, a

cutting-edge tool, and promotes joint development of a rapidly growing

body of mechanised mathematics knowledge. The latter is not only a

center for excellence in CA, but also has lots of expertise in

industrial application of CA.

Before the TP-PL initiative focuses an a proposal text, it seems

appropriate to consider what expertise combined from both institutes

might promise. Such promises are the following.

\subsubsection{Prove properties of technical systems}\label{promise-prove}

Traditionally computers support engineering practice by their

computational power from CA systems or from domain specific

software. As mentioned already, deducing properties of systems from

properties of sub-systems and built-in software traditionally is

concern of personal expertise and common sense.

The progress of pervasive computing drives TP methodology more and

more into hardware systems alongside the integration of software. This

can be observed in mechanical engineering (e.g. autonomous robots

beginning to share the human living and working spaces), electrical

engineering (e.g. in railway signaling systems in the transition to

high-speed trains), etc.

From the users' side the dependability of systems and respective

safety standards create a tendency towards increased use of TP

methodology.

\subsubsection{Improve comparability of algorithms and devices}\label{promise-domain}

Standardised bench-marks are used in disciplines, which are not yet

well settled, which are inherently complex and which are far off

standardisation otherwise. Another way, probably more appropriate with

respect to responsibilities imposed on a working engineer, is FM,

which promotes mechanisation of mathematical/physical theories in

respective axioms, definitions, theorems and proofs in TP technology;

also formal specification of physical entities together with a

thorough formal description of their properties; and also formal

specification of software algorithms together with a thorough formal

description of their properties.

In the academic field FM provides prerequisites for comparing

different kinds of hardware and software systems. Such comparison is

particularly valuable in emerging fields, where an abundance of

different algorithms in combination with various physical devices

are emerging.

\subsubsection{Support assembly of sub-systems}\label{promise-assembly}

Comparison of software algorithms and technical devices on a formal

level provides improved prerequisites for assembling systems from

sub-systems. The COMPASS

project~\footnote{\url{http://www.compass-research.eu}} project even

states commercial reasons for FM: ``Although there are great

opportunities here, the design of innovative products and services

that take advantage of Systems of Systems (SoS) technology is hampered

by the complexity caused by the heterogeneity and independence of the

constituent systems, and the difficulty of communication between their

diverse stakeholders. Developers lack models and tools to help make

trade-off decisions during design and evolution leading to sub-optimal

design and rework during integration and in service. Our work is

inspired by the vision that complex SoSs can be successfully and

cost-effectively engineered using methods and tools that promote the

construction and early analysis of models.''

\subsubsection{Automatically generate verified code}\label{promise-codegen}

is an appealing

feature in engineering anytime. As soon as TP-based domain engineering

has created a sufficiently large and re-usable body of mechanised

knowledge, TP-based software development might become sufficiently

efficient for specific areas of engineering practice. However, a

program, as developed within a TP-based environment, is very

inefficient in execution time and memory consumption within the

TP-based environment.

So extension of Isabelle's code generator to the full range of the

TP-based programming language is a feature very appealing to

engineers.

\subsection{Examples for promising TP-PL applications}

The previous section stated general promises of FM in a long-term

view; the TP-PL project, however, addresses only a small (however

crucial) part of FM, and also wants to have a successful short-term

application.

So several institutes at Graz University of Technology have been

contacted during preparation of the TP-PL project. Presentation of the

general promises discussed in the previous section, identified some

topics in some institutes, which probably could lead to a reasonable

application of the TP-PL. The following topics are notable.

\subsubsection{Electrical Capacitance Tomography}

``Electrical Capacitance Tomography (ECT) is a well-investigated and

well-documented method to non-invasively determine the permittivity

distribution in a pipe and to provide cross-sectional images of this

distribution. The permittivity distribution is obtained by measuring

the electrical capacitance between sets of electrodes placed on the

outer circumference of a non-conductive pipe section. This procedure

leads to a nonlinear and ill-posed inverse problem, where the number

of unknowns (i.e. pixel number) typically exceeds the number of

independent equations (i.e. different pairs of

electrodes).''~\cite{zangl:ect-precomp-12}.

``ECT is well-suited for industrial processes since materials

typically involved in industrial processes like multiphase flows show

good contrast in terms of the permittivity. [..]. Examples of

processes including multiphase flow can be found in almost every

industry, e.g. food production, separation columns, fluidized beds,

chemical reactors, oil production, waste water treatment, mining

operations, and pneumatic

conveying.''~\cite{SpringerBuch-TODO-PERMISSION}. There are many other

applications of ECT, for instance distance sensing in automotive

applications~\cite{zangl:auto-ect-11}.

\medskip The ill-posed inverse problem is tackled by various

mathematical methods in ECT. The ``forward problem'' is

\begin{equation} \label{ect-fwd-pbl}

Y=F(\epsilon)+w\;\;\;\;\;\epsilon\in E\;\;\;\;\;Y\in M

\end{equation}

where $Y$ is the matrix of capacitances in the electrodes, an element

of the measurement space $M$, $\epsilon$ is a matrix in the set of

permittivity distribution spaces $E$, and $w$ represents the

inevitable measurement noise. So, $F$ computes the capacitances $Y$

from the permittivities $\epsilon$ for a certain configuration of

objects. Now, the result expected from ECT is solving the inverse

problem

\begin{equation} \label{ect-inv-pbl}

\epsilon=F^{-1}(Y)

\end{equation}

where the configuration of objects (i.e. the respective permittivity

distribution $\epsilon$) is reconstructed from the measurements $Y$ in

the electrodes. Due to the ill-posedness of the problem and the

measurement noise $w$, a specific reconstruction $F^{-1}_i$ of a

specific distribution $\epsilon_i$ deviates to some

$\hat{\epsilon}_i$ and we get

\begin{equation} \label{ect-estimate}

E\left(\left(\hat{\epsilon}_i-\epsilon_i\right)^2\right)<\delta\;\;\;\;\;\hat{\epsilon}_i=F^{-1}_i(Y)

\end{equation}

where the \textit{expectation} $E$ for the \textit{mean square error}

(or some other quality measure) should be bounded by some

$\delta$. For tackling the inverse $F^{-1}$ various mathematical

methods and various combinations of methods are adopted: linear and

non-linear, iterative and non-iterative, analytic (e.g. derivatives)

and stochastic, continuous and discrete (e.g. the Finite Element

Method (FME)) methods.

As is typical for an emerging field, in ECT there is not yet agreement

on optimal methods for the many possibilities of configurations of

observables. Rather, a typical publication of yet another method

presents a configurations of observables, where this method is

superior --- but it can hardly be compared with other methods: general

investigations are still missing. For instance, given a certain

$\delta$ in the inequality (\ref{ect-estimate}) above, for which kinds

of $Y$ which kinds of $F^{-1}_i$ are below $\delta$. Or is there a

$\delta$ such that for a given $Y$ we have $\forall

F^{-1}_i.\;F^{-1}_i(Y)\geq\delta$, i.e. there are technical reasons

which do not allow for this specific $Y$ to have a better

approximation then $\delta$? Or the other way round: for some $\delta$

and some reconstruction method $F^{-1}_i$, do we have $\forall

Y.\;F^{-1}_i(Y)\geq\delta$, i.e. the method $F^{-1}_i$ is limited to

an error above $\delta$? Even general knowledge would be useful like:

for a certain $Y$ and a certain $F^{-1}_i$ can we have $\exists

\delta.\; {\it max}\left(\hat{\epsilon}_i-\epsilon_i \right)$,

i.e. can we expect reasonable data at all? Answering such questions

concerns hardware and software components included in $F^{-1}$.

\bigskip As an example, at TUG there is ongoing

research~\cite{zangl:ect-precomp-12} on a specific method, which

pre-computes a matrix $A$ such that process monitoring, as the very

task of ECT and probably implemented in large quantities of devices,

becomes simply

\begin{equation} \label{ect-online}

\hat{\epsilon}=H\,A

\end{equation}

where $H$ contains the actual measurements subjected to

computationally cheap methods; so, monitoring does neither involve

iterations nor expensive methods like Gauss-Newton reconstruction. For

this method the experimental data are excellent when compared to the

state-of-the-art; general statements about the method's properties are

to be researched, hopefully supported by TP technology. Interesting

for practical application is validation of this method, which

specifies general questions asked above to $\exists

A.\;E\left(\left(\hat{\epsilon}_i-\epsilon_i\right)^2\right)<\delta$,

or more simple ${\it max}\left(\hat{\epsilon}_i-\epsilon_i

\right)<\delta$.

The method for calculating $A$ comprises hardware and software

components, the respective specification is as follows.

\begin{spacing}{1}

\begin{center}

%\begin{tabular}{ | l | l | p{8cm} |}

\begin{tabular}{ | l | l | l |}

\hline

& variable & property / \textit{explanation} \\\hline

input & & \\\hline

& $K_i$ & quadratic, positive semi-definite matrix \\

& & computed by a specific generator \cite{zangl:ect-precomp-12}~p.6, \\

& & \textit{which creates a specific PDF and which} \\

& & \textit{reflects the specific PDF with respect to a specific FEM geometry} \\\hline

& $\tilde{K}$ & TODO \\\hline

& $R$ & \textit{matrix of constraints;} \\

& & \textit{reflects the sensor geometry within a specific FEM geometry} \\\hline

& $\hat{e}$ & \textit{matrix of estimated values in the image space $E$}\\\hline

output& & \\\hline

& $A$ & \textit{coefficient matrix for reconstruction of pixels} \\\hline

\end{tabular}

\end{center}

\end{spacing}

The calculation of $A$ follows equalities on matrices, in detail

$R=K\cdot U$ where $K=\Sigma_{i=1}^l e_i K_i$ and $H=\tilde{K}\cdot U$

where $\tilde{K}=\Sigma_{i=1}^l e_i \tilde{K_i}$, leading to

$A=(H^TH)^{-1}H^T\check{E}$ finally. By Monte Carlo Method (MCM) $l$

samples $\check{E}$ are generated; for $l=10.000$ the dimensions are

$121\times 316$ for $A$, $50.000\times 121$ for $H$ and $50.000\times

316$ for $\check{E}$ respectively.

%was ist $U$?

%H in (4) ist was anderes als H oberhalb

\bigskip Summary: ECT is a topic which promises some success in all points

addressee in the previous section:

\begin{enumerate}

\item \textit{Prove properties of technical systems,} (\S\ref{promise-prove}) this is

desirable for the example given above.

\item \textit{Improve comparability of algorithms and devices} (\S\ref{promise-domain}) is an

actual issue in the emerging field of ECT. Some initial contributions

by the TP-PL project seem possible.

\item \textit{Automatically generate verified code} (\S\ref{promise-codegen}) for software

meeting stardardisation criteria, that is an ongoing concern in

development of measurement devices.

\item \textit{Support assembly of sub-systems} (\S\ref{promise-assembly}) is beyond the scope of

the TP-PL project, but of principal interest: some applications like

automotive applications are subject to

dependability~\cite{zangl:auto-ect-11}, others are subject to

standards for measurement devices.

\end{enumerate}

\subsubsection{Dependability issues in Robotics}

``When autonomous robots begin to share the human living and working

spaces, safety becomes paramount. It is legally required that the

safety of such systems is ensured, e. g. by certification according

to relevant standards such as IEC 61508''~\footnote{Cited from

\cite{isa-robot-12}.}.

\medskip At TUG there are several activities in robotics.

\subsubsection{Non-Shannon-type inequalities}

Another domain where TP-PL seems to be able to serve actual research is

Information theory -- in spite the fact, that the Isabelle theory

\textit{Information.thy} in the release of 2012 covers only the first

50 pages of total 650 in a standard text book~\cite{info-thy-06}: the

final theorems in \textit{Information.thy} are

\textit{mutual\_information\_eq\_entropy\_conditional\_entropy,

conditional\_entropy\_less\_eq\_entropy, entropy\_chain\_rule} and

\textit{entropy\_data\_processing}.

What makes this topic promising, is request for automated provers for

so-called ``Shannon-type inequalities'' --- however, there are also

``non-Shannon-type inequalities''~\cite{non-shannon-01} which would

require interactive proof.

\subsection{Summary: Which goals are realisable in the TP-PL project~?}

.\\.\\.\\TODO

\section*{Abbreviations}

\begin{spacing}{1}

\begin{center}

\begin{tabular}{l | l}

ECT & electrical capacitance tomography \\

FEM & finite element method \\

MCM & monte carlo method \\

PDF & probability density function \\

& \\

& \\

\end{tabular}

\end{center}

\end{spacing}%from{tabular}

\end{spacing}%from\begin{document}

\begin{spacing}{1}\bibliography{references}\end{spacing}

\end{document}

% * support for agreements in project planning:

% * What is the TPPL prototype good for ?

% * What are general directions of development for successors ?

% * Reflect possibly different views of TP, software verification and CA

% * raw material for proposal

\documentclass[11pt,a4paper]{scrartcl}

\usepackage{ucs}

\usepackage[utf8x]{inputenc}

\usepackage[onehalfspacing]{setspace}

\usepackage{paralist}

\usepackage{url}

\bibliographystyle{alpha}

\usepackage{graphicx}

\usepackage{sty/editing} %DISABLE FOR FINAL VERSION

\title{Design and Prototype for a \\

TP-based Programming Language\\

{\Large Draft for an FWF proposal}}

\begin{document}

\begin{spacing}{1}

\tableofcontents

\bigskip \bigskip

\section{Theorem Proving underway to Engineering Practice}

% This section picks out the note ``that the aim of this project is to

% provide a running prototype environment'' in \S\ref{mission} and goes

% beyond the mission stated there.

Interdisciplinary work as addressed in the proposal ``Design and

Prototype for a TP-based Programming Language (TP-PL)'' is best begun

by sharing visions between TP-PL developers and potential users. Such

visions shall be a fertile soil for joint work to identify applications

of TP-PL, which create a win-win situation for users and developers.

These notes shall

serve this purpose and start from a wider perspective going beyond the

proposal text.

\subsection{Engineers' attitudes towards mathematical software}

In applied sciences there are strong attitudes towards usage of

mathematical software which in turn are a constituent part of

professional values and ethics.

A first aspect of the attitudes reflects a great success of computer

mathematics, in numeric as well as in symbolic computation: Engineers

and experts in applied sciences have high expectations with regard to

computational power of tools like Mathematica, Mathlab or Maple, for

instance when solving huge equational systems, when performing

enormous numbers of computations or when simplifying large terms.

A second aspect of the attitudes addresses deficiencies of

mathematical software still considered inevitable: Engineers are

taught to be personally responsible for results of mathematical

software and to be always alert for casual inappropriate results due

to ill-conditioned systems, e.g.~numerical instabilities with floating

point numbers or issues related to multivalued functions

\cite{davenport-10:multivalued}~\footnote{Errors cited from

\cite{hoelzl09realineequalities}

are $\int^1_{-1}{\sqrt{x^2}dx}=0$ instead of $=1$ (Maple, \url{http://www.maplesoft.com/products/Maple/}) and

$\int^1_{-1}{\frac{1}{\sqrt{x^2}}dx}=0$ instead of ``undefined''

(Mathematica, \url{http://www.wolfram.com/mathematica/}).}.

\medskip So these traditional attitudes and expectations have good

reasons and must be taken into account when TP is approaching

engineering practice.

\subsection{Computer Mathematics' approaches to engineering practice}

There are several success stories of rigorous formal approaches to

engineering problems with impact on practice.

TP is particularly successful in software verification \footnote{A representative

overview can be gained from the publication lists of the Verisoft project

at \url{http://www.verisoft.de/PublikationSeite.html}},

but has also gained revenue in mechanised proofs for sizable mathematical

problems, e.g.~the Kepler Conjecture\footnote{\url{http://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet}}

or the Four Colour Theorem \cite{DBLP:conf/ascm/Gonthier07}.

Success stories of certified and verified Computer Algebra are

\cite{TODO-verified-CA}.

\footnote{fixme[Further success stories of CA?]}

\bigskip Apart from the approaches by the dedicated academic

communities from TP and from CA respectively there are further

approaches with similar goals. One integrative approach from the side of computer

science is called ``Formal Methods

(FM)''~\cite{fm-03}~\footnote{http://www.fmeurope.org/}, an approach

which actually has been born in Austria and which is still alive as

``Vienna Development Method

(VDM)''~\cite{vdm-09}~\footnote{http://www.vdmportal.org/twiki/bin/view}.

This community promotes several successful projects, for instance the

COMPASS project~\footnote{www.compass-research.eu} with the goal of

supporting the engineering of dependable systems-of-systems based on

contractual styles of interface specification. Proof support is under

development and ``is expected to build on HOL''~\fixme[Which HOL? Reference imprecise.]~\footnote{Deliverable

D33.2 ``Theorem Proving Support'' at

http://www.compass-research.eu/deliverables.html.}. These goals are

close to those of the TP-PL project such that the proposal has to

refer to such projects.

\medskip Another approach from the side of applied mathematics is

called ``Systems Modeling (SM)'' split into various directions from

Operational Research to such specific technologies like

``Vehicle Systems Model-ling and

Testing''~\footnote{http://www.inderscience.com/jhome.php?jcode=ijvsmt}.

These approaches build on graphical representations of problems and

solutions rather than on representation based on formal logic. From

this side come easy-to-adopt mathematical tools like Maple's

MapleSim~\footnote{http://www.maplesoft.com/products/maplesim} and

Mathematica's System

Modeler~\footnote{http://www.wolfram.com/system-modeler}.

\subsection{What are the promises of TP + CA?}

A generally promising aspect of the TP-PL proposal is that explicit

cooperation is established between two institutes, Theorem Proving

Group at TUM and Research Institute for Symbolic Computation at JKU,

each leading in the respective domain: The former develops Isabelle, a

cutting-edge tool, and promotes joint development of a rapidly growing

body of mechanised mathematics knowledge. The latter is not only a

center for excellence in CA, but also has lots of expertise in

industrial application of CA.

Before the TP-PL initiative focuses an a proposal text, it seems

appropriate to consider what expertise combined from both institutes

might promise. Such promises are the following.

\subsubsection{Prove properties of technical systems}\label{promise-prove}

Traditionally computers support engineering practice by their

computational power from CA systems or from domain specific

software. As mentioned already, deducing properties of systems from

properties of sub-systems and built-in software traditionally is

concern of personal expertise and common sense.

The progress of pervasive computing drives TP methodology more and

more into hardware systems alongside the integration of software. This

can be observed in mechanical engineering (e.g. autonomous robots

beginning to share the human living and working spaces), electrical

engineering (e.g. in railway signaling systems in the transition to

high-speed trains), etc.

From the users' side the dependability of systems and respective

safety standards create a tendency towards increased use of TP

methodology.

\subsubsection{Improve comparability of algorithms and devices}\label{promise-domain}

Standardised bench-marks are used in disciplines, which are not yet

well settled, which are inherently complex and which are far off

standardisation otherwise. Another way, probably more appropriate with

respect to responsibilities imposed on a working engineer, is FM,

which promotes mechanisation of mathematical/physical theories in

respective axioms, definitions, theorems and proofs in TP technology;

also formal specification of physical entities together with a

thorough formal description of their properties; and also formal

specification of software algorithms together with a thorough formal

description of their properties.

In the academic field FM provides prerequisites for comparing

different kinds of hardware and software systems. Such comparison is

particularly valuable in emerging fields, where an abundance of

different algorithms in combination with various physical devices

are emerging.

\subsubsection{Support assembly of sub-systems}\label{promise-assembly}

Comparison of software algorithms and technical devices on a formal

level provides improved prerequisites for assembling systems from

sub-systems. The COMPASS

project~\footnote{\url{http://www.compass-research.eu}} project even

states commercial reasons for FM: ``Although there are great

opportunities here, the design of innovative products and services

that take advantage of Systems of Systems (SoS) technology is hampered

by the complexity caused by the heterogeneity and independence of the

constituent systems, and the difficulty of communication between their

diverse stakeholders. Developers lack models and tools to help make

trade-off decisions during design and evolution leading to sub-optimal

design and rework during integration and in service. Our work is

inspired by the vision that complex SoSs can be successfully and

cost-effectively engineered using methods and tools that promote the

construction and early analysis of models.''

\subsubsection{Automatically generate verified code}\label{promise-codegen}

is an appealing

feature in engineering anytime. As soon as TP-based domain engineering

has created a sufficiently large and re-usable body of mechanised

knowledge, TP-based software development might become sufficiently

efficient for specific areas of engineering practice. However, a

program, as developed within a TP-based environment, is very

inefficient in execution time and memory consumption within the

TP-based environment.

So extension of Isabelle's code generator to the full range of the

TP-based programming language is a feature very appealing to

engineers.

\subsection{Examples for promising TP-PL applications}

The previous section stated general promises of FM in a long-term

view; the TP-PL project, however, addresses only a small (however

crucial) part of FM, and also wants to have a successful short-term

application.

So several institutes at Graz University of Technology have been

contacted during preparation of the TP-PL project. Presentation of the

general promises discussed in the previous section, identified some

topics in some institutes, which probably could lead to a reasonable

application of the TP-PL. The following topics are notable.

\subsubsection{Electrical Capacitance Tomography}

``Electrical Capacitance Tomography (ECT) is a well-investigated and

well-documented method to non-invasively determine the permittivity

distribution in a pipe and to provide cross-sectional images of this

distribution. The permittivity distribution is obtained by measuring

the electrical capacitance between sets of electrodes placed on the

outer circumference of a non-conductive pipe section. This procedure

leads to a nonlinear and ill-posed inverse problem, where the number

of unknowns (i.e. pixel number) typically exceeds the number of

independent equations (i.e. different pairs of

electrodes).''~\cite{zangl:ect-precomp-12}.

``ECT is well-suited for industrial processes since materials

typically involved in industrial processes like multiphase flows show

good contrast in terms of the permittivity. [..]. Examples of

processes including multiphase flow can be found in almost every

industry, e.g. food production, separation columns, fluidized beds,

chemical reactors, oil production, waste water treatment, mining

operations, and pneumatic

conveying.''~\cite{SpringerBuch-TODO-PERMISSION}. There are many other

applications of ECT, for instance distance sensing in automotive

applications~\cite{zangl:auto-ect-11}.

\medskip The ill-posed inverse problem is tackled by various

mathematical methods in ECT. The ``forward problem'' is

\begin{equation} \label{ect-fwd-pbl}

Y=F(\epsilon)+w\;\;\;\;\;\epsilon\in E\;\;\;\;\;Y\in M

\end{equation}

where $Y$ is the matrix of capacitances in the electrodes, an element

of the measurement space $M$, $\epsilon$ is a matrix in the set of

permittivity distribution spaces $E$, and $w$ represents the

inevitable measurement noise. So, $F$ computes the capacitances $Y$

from the permittivities $\epsilon$ for a certain configuration of

objects. Now, the result expected from ECT is solving the inverse

problem

\begin{equation} \label{ect-inv-pbl}

\epsilon=F^{-1}(Y)

\end{equation}

where the configuration of objects (i.e. the respective permittivity

distribution $\epsilon$) is reconstructed from the measurements $Y$ in

the electrodes. Due to the ill-posedness of the problem and the

measurement noise $w$, a specific reconstruction $F^{-1}_i$ of a

specific distribution $\epsilon_i$ deviates to some

$\hat{\epsilon}_i$ and we get

\begin{equation} \label{ect-estimate}

E\left(\left(\hat{\epsilon}_i-\epsilon_i\right)^2\right)<\delta\;\;\;\;\;\hat{\epsilon}_i=F^{-1}_i(Y)

\end{equation}

where the \textit{expectation} $E$ for the \textit{mean square error}

(or some other quality measure) should be bounded by some

$\delta$. For tackling the inverse $F^{-1}$ various mathematical

methods and various combinations of methods are adopted: linear and

non-linear, iterative and non-iterative, analytic (e.g. derivatives)

and stochastic, continuous and discrete (e.g. the Finite Element

Method (FME)) methods.

As is typical for an emerging field, in ECT there is not yet agreement

on optimal methods for the many possibilities of configurations of

observables. Rather, a typical publication of yet another method

presents a configurations of observables, where this method is

superior --- but it can hardly be compared with other methods: general

investigations are still missing. For instance, given a certain

$\delta$ in the inequality (\ref{ect-estimate}) above, for which kinds

of $Y$ which kinds of $F^{-1}_i$ are below $\delta$. Or is there a

$\delta$ such that for a given $Y$ we have $\forall

F^{-1}_i.\;F^{-1}_i(Y)\geq\delta$, i.e. there are technical reasons

which do not allow for this specific $Y$ to have a better

approximation then $\delta$? Or the other way round: for some $\delta$

and some reconstruction method $F^{-1}_i$, do we have $\forall

Y.\;F^{-1}_i(Y)\geq\delta$, i.e. the method $F^{-1}_i$ is limited to

an error above $\delta$? Even general knowledge would be useful like:

for a certain $Y$ and a certain $F^{-1}_i$ can we have $\exists

\delta.\; {\it max}\left(\hat{\epsilon}_i-\epsilon_i \right)$,

i.e. can we expect reasonable data at all? Answering such questions

concerns hardware and software components included in $F^{-1}$.

\bigskip As an example, at TUG there is ongoing

research~\cite{zangl:ect-precomp-12} on a specific method, which

pre-computes a matrix $A$ such that process monitoring, as the very

task of ECT and probably implemented in large quantities of devices,

becomes simply

\begin{equation} \label{ect-online}

\hat{\epsilon}=H\,A

\end{equation}

where $H$ contains the actual measurements subjected to

computationally cheap methods; so, monitoring does neither involve

iterations nor expensive methods like Gauss-Newton reconstruction. For

this method the experimental data are excellent when compared to the

state-of-the-art; general statements about the method's properties are

to be researched, hopefully supported by TP technology. Interesting

for practical application is validation of this method, which

specifies general questions asked above to $\exists

A.\;E\left(\left(\hat{\epsilon}_i-\epsilon_i\right)^2\right)<\delta$,

or more simple ${\it max}\left(\hat{\epsilon}_i-\epsilon_i

\right)<\delta$.

The method for calculating $A$ comprises hardware and software

components, the respective specification is as follows.

\begin{spacing}{1}

\begin{center}

%\begin{tabular}{ | l | l | p{8cm} |}

\begin{tabular}{ | l | l | l |}

\hline

& variable & property / \textit{explanation} \\\hline

input & & \\\hline

& $K_i$ & quadratic, positive semi-definite matrix \\

& & computed by a specific generator \cite{zangl:ect-precomp-12}~p.6, \\

& & \textit{which creates a specific PDF and which} \\

& & \textit{reflects the specific PDF with respect to a specific FEM geometry} \\\hline

& $\tilde{K}$ & TODO \\\hline

& $R$ & \textit{matrix of constraints;} \\

& & \textit{reflects the sensor geometry within a specific FEM geometry} \\\hline

& $\hat{e}$ & \textit{matrix of estimated values in the image space $E$}\\\hline

output& & \\\hline

& $A$ & \textit{coefficient matrix for reconstruction of pixels} \\\hline

\end{tabular}

\end{center}

\end{spacing}

The calculation of $A$ follows equalities on matrices, in detail

$R=K\cdot U$ where $K=\Sigma_{i=1}^l e_i K_i$ and $H=\tilde{K}\cdot U$

where $\tilde{K}=\Sigma_{i=1}^l e_i \tilde{K_i}$, leading to

$A=(H^TH)^{-1}H^T\check{E}$ finally. By Monte Carlo Method (MCM) $l$

samples $\check{E}$ are generated; for $l=10.000$ the dimensions are

$121\times 316$ for $A$, $50.000\times 121$ for $H$ and $50.000\times

316$ for $\check{E}$ respectively.

%was ist $U$?

%H in (4) ist was anderes als H oberhalb

\bigskip Summary: ECT is a topic which promises some success in all points

addressee in the previous section:

\begin{enumerate}

\item \textit{Prove properties of technical systems,} (\S\ref{promise-prove}) this is

desirable for the example given above.

\item \textit{Improve comparability of algorithms and devices} (\S\ref{promise-domain}) is an

actual issue in the emerging field of ECT. Some initial contributions

by the TP-PL project seem possible.

\item \textit{Automatically generate verified code} (\S\ref{promise-codegen}) for software

meeting stardardisation criteria, that is an ongoing concern in

development of measurement devices.

\item \textit{Support assembly of sub-systems} (\S\ref{promise-assembly}) is beyond the scope of

the TP-PL project, but of principal interest: some applications like

automotive applications are subject to

dependability~\cite{zangl:auto-ect-11}, others are subject to

standards for measurement devices.

\end{enumerate}

\subsubsection{Dependability issues in Robotics}

``When autonomous robots begin to share the human living and working

spaces, safety becomes paramount. It is legally required that the

safety of such systems is ensured, e. g. by certification according

to relevant standards such as IEC 61508''~\footnote{Cited from

\cite{isa-robot-12}.}.

\medskip At TUG there are several activities in robotics.

\subsubsection{Non-Shannon-type inequalities}

Another domain where TP-PL seems to be able to serve actual research is

Information theory -- in spite the fact, that the Isabelle theory

\textit{Information.thy} in the release of 2012 covers only the first

50 pages of total 650 in a standard text book~\cite{info-thy-06}: the

final theorems in \textit{Information.thy} are

\textit{mutual\_information\_eq\_entropy\_conditional\_entropy,

conditional\_entropy\_less\_eq\_entropy, entropy\_chain\_rule} and

\textit{entropy\_data\_processing}.

What makes this topic promising, is request for automated provers for

so-called ``Shannon-type inequalities'' --- however, there are also

``non-Shannon-type inequalities''~\cite{non-shannon-01} which would

require interactive proof.

\subsection{Summary: Which goals are realisable in the TP-PL project~?}

.\\.\\.\\TODO

\section*{Abbreviations}

\begin{spacing}{1}

\begin{center}

\begin{tabular}{l | l}

ECT & electrical capacitance tomography \\

FEM & finite element method \\

MCM & monte carlo method \\

PDF & probability density function \\

& \\

& \\

\end{tabular}

\end{center}

\end{spacing}%from{tabular}

\end{spacing}%from\begin{document}

\begin{spacing}{1}\bibliography{references}\end{spacing}

\end{document}