[SystemSafety] Logic

[Les Chambers]

Peter
I am in furious agreement with Steve Tockey. If we are to deal effectively
with the large code bodies that are now the norm. We must find a way to
bring formal methods out of the lab and into general use. 
The primary reason for this is that the larger a code body becomes the less
likely it is that anyone but the author will ever review the code. Ask your
formal methods detractors, "do you really want to sit on an aircraft with
avionics software that has been eyeballed by only one person - the author?"
I have done enough test work to be fully conversant with the ugliness that
some programmers are capable of. Believe me, you do not want to be anywhere
near a life critical software intensive system infused by same. 
Of course I am assuming here that formal methods support automated static
and possibly dynamic code review. Am I correct? 
I know from personal experience that manual review of very complex designs
and code is substantially simplified by semiformal methods such as state
machines.

The mission of any engineering discipline is to reduce science to practice
to solve real world problems. Unfortunately the profession seems to be stuck
at semiformal methods.
The current impediment is money; finding investors who want to pay for the
software engineer to formally specify program before it's written. 
On one missile program I worked on it was hard enough to get the cash to
keep the mission function flow diagrams up-to-date, let alone specify
anything with formal methods.
Simplification and maybe tool support is the solution. I hope that's
possible - over to you.
If we could abstract this problem in terms of human commercial behaviour,
industry experience with state engines is a good case study. Vendors of
programmable logic controllers took a commercial decision to emulate relay
racks described by ladder diagrams when they first released their products.
This allowed existing electricians to use the new tools with minimal
training. They could have followed the other option of logical decomposition
of all control problems into cooperating state engines. That would have
required retraining of the entire cohort of electrical tradesmen and, as
such, would probably have been commercial suicide. 
Of late, some products do support the state engine concept though the last
one I came across was a really ugly implementation.
In the period 1975 to 1985 I worked in an environment where all control
systems were implemented with cooperating state engines. We simplified the
concept so plant operators could easily understand what was going on. We
never did use the word State. We used step. We didn't use the phrase state
engine. We used the term sequence control unit. Operators understood that.
That's how operator manuals were organised. After a few years we even had
operators - with no high school education, who had run a state based
machinery and learnt the concepts by doing - writing control programs.
Is this possible with formal methods? This is a righteous question that I
would like to see answered by the enormous cohort of brainpower corralled in
the world's universities. A solution would be hugely beneficial to the
industry at large. 
My humble suggestion for a starting point is to start with something that
programmers know and move on from there.
I am passionate about this subject because, in a previous life, I was the
poor electrician responsible for figuring out how a room full of relay racks
was controlling a high-speed lift (elevator). The massive complexity of
these control systems required 2 to 3 years practical experience before you
became useful. It was a craft with high priests who "had the knowledge" and
walked on water. Much like current practitioners of formal methods. That
does not have to be. State engines simplify. State engines support analysis
of design. I hope the same will be true one day for upsidedown As and
backward Es.
In the meantime, the joint ACM, IEEE task force , who recently released
their latest curriculum guidelines for undergraduate degree programmes in
computer science are very supportive of teaching formal methods in their
software engineering modules. See:
http://www.acm.org/education/CS2013-final-report.pdf
I hope this helps.

Go Peter.

Cheers
Les

-----Original Message-----
From: systemsafety-bounces at lists.techfak.uni-bielefeld.de
[mailto:systemsafety-bounces at lists.techfak.uni-bielefeld.de] On Behalf Of
Peter Bernard Ladkin
Sent: Saturday, February 15, 2014 8:53 PM
To: systemsafety at techfak.uni-bielefeld.de
Subject: [SystemSafety] Logic

Folks,

we have a local issue in our faculty which I think is of more general
importance and would like to
solicit views, evidence and so forth. This is about curricula; I don't know
how many people here are
interested in that at the undergrad level, and crave indulgence from those
who don't.

To put the last paragraph first, I would like to gather opinions on the
necessity of some skills. I
would argue that programming dependable systems, and dependable-software
engineering in general,
requires some facility with formal description languages (FDLs). FDLs are
necessary for requirements
specification and analysis, and they are also necessary for the refinement
steps that occur between
requirements and code, as well as for any kind of static analysis of code.
They are necessary for
validating compilers. Classical proposition and predicate logics count
amongst the most common and
basic FDLs; a skill in expressing some kinds of assertions in predicate
logic has often been
regarded as necessary for a basic informatics education. I would think some
understanding of how
FDLs work is essential for any work in dependable engineering of SW. Do
people agree? If so, could
you please give me some evidence?

The context is this.

I am on various mailing lists for announcements of conferences and academic
research jobs (PhDs and
Post-docs). Almost all of the stuff I see requires some to considerable
expertise in formal methods
(FM). Indeed, I would say that support for FM-related research has exploded
in the last ten years.
But our students don't have enough experience of FM in their degree courses
to stand much of a
chance applying for such jobs. Even if they take all I regularly offer, it
is barely enough.

We have four undergraduate degree programs, all "hyphen-informatics" in
which informatics is studied
along with an application domain: informatics in natural sciences (NWI);
bioinformatics and genomics
(BG); "cognitive informatics" (KOI); and media informatics (MI). (The last
one of these is aimed
primarily at new-media artists - selection is through an artistic
portfolio.)

We used to have degree programs based on the German Diplom system
(equivalent to a Master's with
thesis, but as a first degree) but have switched in the last decade to
(Germany's idea of)
Bachelor's/Master's combination.

The course in Theoretical Informatics (TheoInf) used to be compulsory (for
all except media
informatics), and comprised the usual automata theory, Chomsky-hierarchy
languages and logic. We
agreed a few years ago to separate logic from the other two subjects and
have two courses. This
decision was based partly on the fact that I had developed an applied-logic
module (= two courses in
two semesters) which did rather more than the somewhat cursory nod (from my
point of view) it got in
the combined course.

But something odd happened that nobody I asked has been able to explain.
TheoInf is compulsory for
NWI and KOI, as it should be. But Applied Logic did not become compulsory
for anyone. So,
essentially, logic became an elective.

Boolean logic is taught in the Technical Informatics module, which is
compulsory for NWI and KOI
(the other two get a brief survey of TechInf), which does the usual
Karnaugh-diagram and
Quine-McCluskey minimisation stuff. But there is the question whether people
who study Boolean logic
for TechInf can apply what they learn to Propositional Logic in the form of
language rather than
algebra.

Logic is also briefly, very cursorily, mentioned in the Mathematics modules
required for NWI and
KOI, which are taught by the Maths Department, but not to the extent that
any student feels they can
use it.

My indications from a decade ago were that our students couldn't, very well
(I didn't teach TheoInf,
but I used to examine for it. I would give an exam question - "what does (A
AND B OR C) mean, where
A,B and C are propositions". The answer is twofold: that the meaning of a
statement in propositional
logic is given by its truth table; and further that there are two possible
truth tables
corresponding to this statement. Less than half could give the first answer,
and only about one in
five would notice the ambiguity. This despite asking the *same question* for
years and years). This
is why I developed my Applied Logic course, to get people familiar with the
basics of inference
(syntax) and meaning (semantics). The first semester is coextensive with,
say, Huth and Ryan Section
1.2.

One of my Bachelor's students (that is, a student who has done a number of
electives which my group
offers, and has subsequently tutored the courses) applied to do a Master's
at another German
university (the Technical University of Braunschweig) and was told he didn't
appear to have enough
logic. He told them he was currently taking my Applied Logic course, as well
as another course in
logic in the Philosophy department, and he was then provisionally admitted
(he did end up staying
with us, though).

I suggested to my colleagues that we didn't appear to be teaching all of the
basic material which
other informatics people would expect from people with a degree in
Informatics, and that it would be
a good idea at least to inform students of what electives they might need in
addition to compulsory
material in order pursue a Master's in Informatics elsewhere. We had some
discussion of that.

At least some colleagues seem to think that we offer broadly what the
professional society (GI)
recommends in curricula. That may formally be so, but I would say only
formally. It also doesn't
address the issue of what kind of skill with FDLs people with a university
degree in informatics
could be expected to have.

I looked at the curricula of three top-20 universities in the UK: Oxford,
Cambridge and Imperial
College London. All of them have substantial logic in their curricula for
any of the degree courses.
(Oxford seems to have logic in about half its electives as well!).

I have started to contact people who are likely to feel similarly about the
importance of skills
with FDLs and in particular with applied logic in informatics as I do. I'd
be grateful for any
material - stories, opinions, observations about curricula, about software
engineering practice, and
so forth - which you may be able to convey.

PBL


Prof. Peter Bernard Ladkin, Faculty of Technology, University of Bielefeld,
33594 Bielefeld, Germany
Tel+msg +49 (0)521 880 7319  www.rvs.uni-bielefeld.de




_______________________________________________
The System Safety Mailing List
systemsafety at TechFak.Uni-Bielefeld.DE