Re: [SystemSafety] Logic

From: Les Chambers < >
Date: Sun, 16 Feb 2014 15:42:03 +1000


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_xxxxxx [mailto:systemsafety-bounces_at_xxxxxx Peter Bernard Ladkin
Sent: Saturday, February 15, 2014 8:53 PM To: systemsafety_at_xxxxxx 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_xxxxxx

The System Safety Mailing List
systemsafety_at_xxxxxx Received on Sun Feb 16 2014 - 06:42:27 CET

This archive was generated by hypermail 2.3.0 : Fri Feb 22 2019 - 15:17:06 CET