[SystemSafety] The States and Modes debate

[Steve Tockey]

Les wrote,

“State charts are a visual formalism, though not a formal method.”

I would refer you to:

Jeanette M. Wing, A Specifiers Introduction to Formal Methods, Computer, Vol 23, Issue 9, pp8-23, 1990.

You can find it here: https://www.cs.cmu.edu/~wing/publications/Wing90a.pdf

Her key point is that so long as you have an adequate mapping to a consistent underlying mathematics-based formalism then it’s perfectly fine to be using a easily-human-consumable surface notations and still be sufficiently “formal”. You just need to be explicit somewhere about stating what that notation to formalism mapping is (e.g., Appendix L in my second book). Just because it’s a drawing does not necessarily mean it can’t be reasoned about formally. In fact, I would claim, such a drawing needs to be able to be reasoned about formally or it’s not very useful—particularly in safety critical situations.

I suspect that in your case the mapping from drawings to the underlying formalisms was there implicitly, just not explicitly.


— steve




On May 22, 2026, at 8:03 PM, Les Chambers <les at chambers.com.au> wrote:

Must the Cheshire Cat reappear - sigh!
Peter
RE: “You seem to have a prejudice for working with numbers when it comes to state machines”
You are correct. I do. This originates from 10 years of lived experience, in many chemical processing plants dealing with hundreds of state engines.  A plant would have up to 5 state engines operating in parallel (we called them ”sequence control units (SCUs)” for operator cognition), each comprising around 10 states (we called “steps”). Courtesy of our state chart implementation, walking into a control room, you could determine the complete status of the plant by scanning 3 to 5 current step numbers. A site manager supervising say, five plants, could, in real time, determine the status of his complete chemical processing complex by glancing at a single screen provided by our supervisor systems. Numbers ruled the lives of everyone in the complex. A great shorthand for, "where are we up to?" A small subset of numbers, usually one, would put a chill down your spine, indicating a dangerous condition such as a gas release or an explosive state within a reactor. There could be no ambiguity here. Hence, my violent opposition to synonyms of any kind in a Safety-Critical control system. Your EUC example has no currency in an environment riding herd on a reaction kinetics that can tear your body into subatomic particles or fill your lungs with hydrochloric acid. To be clear, we used one synonym and one synonym only. If you mentioned state or mode in a control room, the operator would stare at you blankly – and a good thing too.
Keeping it that simple was always a great intellectual challenge. In the American operations I worked in, our greatest single challenge was helping plant engineers simplify their state engines, avoiding state explosion. Harel solved this problem with state hierarchy - super-states and sub-states. We avoided this architecture as it would introduce more complexity into operations. Referring to my previous post, we often had operators without a high school education. I got a great kick out of working with these salt-of-the-earth guys. Despite their disinterest in academia, they were, to a man/woman, decent people who were smart and dependable, a non-negotiable attribute for people who ran plants processing dangerous chemicals 24/7 - 16 hours a day with no engineers present. So cognition/ease-of-use were the fundamental objectives of all our control systems. This is why we embraced the simplified state engine - a marvellous invention.

Re: formal methods …. “For almost all formal verification techniques for the last 57 years use them or some equivalent.”
State charts are a visual formalism, though not a formal method. This is the closest we ever got. Our problem was program size, lack of perceived benefit and cognition. The control code was comprehensively documented and became the plant operations manual. You would find a thick pile of fanfold paper on the desk of every control room. Operators could actually read it. The International success of this discipline was directly due to our focus on human beings and understanding. The single greatest success factor was that we had plant engineers write programs and live with them. In this context, teaching them all formal methods was impractical.
If anyone on this list has implemented formal methods in a large system, I would love to hear about the experience.

Your point reminds me of other academic protestations I experienced on a two-year, hundred-million-dollar rail project with SIL 2 subsystems. We were short on V&V staff, so my client company hired many V&V types from a local university research group. They kicked down our door, feisty and arrogant, damming our Jurassic hides for not formally proving all our software. Other than that, they were good, smart kids. We got along well. Over time, I could see their attitudes change as they realised how impractical that approach would be in a project that had tripley redundant supervisory computers communicating with 250 remote terminal control units within embedded systems and micro code configured - all in a constant state of change.

As I fade out … again … I think it is worth reflecting on the future of “correctness” determination in systems as a whole in the context of AI. I recommend a book, The Infinity Machine [1].  It chronicles the rise of Demis Hassabis and DeepMind. Demis’ defining insight in seeking out artificial general intelligence, when all others believed it was impossible, was that human beings are seldom computational engines [1]. They are mostly inductive creatures who have survived through pattern matching, and any attempt at artificial intelligence should follow that path rather than the computational deductive path that we would follow with formal methods. He believes this was the core reason for the failure of symbolic AI in the 1980s and the reason for his team winning at Go, a pattern-matching exercise that is computationally intractable - Legal Positions (State Space) - 10^{172}.
In partnership with Claude code, I am developing a crypto trading platform in JavaScript and Python. I am rusty on JavaScript and have never written Python. I started with good intentions, given that this code will spend my money. I was determined to review every line. I soon gave up, there was too much of it. All my time was spent developing a 74,000-word specification that merged a phased implementation strategy with software requirements and critical architectural decisions. All in partnership with Claude's code, followed by seven cycles of Claude's Fagan review. Research reveals my experience is typical.
What then of formal methods? Given the productivity improvements – I can now achieve in minutes what used to take me days - is this the end of that path? Or only the beginning with AI enhancement of formal methods?
Over to those wiser than me …

Cheers
Les.

[1] Mallaby, Sebastian. The Infinity Machine: Demis Hassabis, DeepMind and the Quest for Superintelligence (p. 25). Penguin Books Ltd. Kindle Edition.
After all, humans engage in deductive logic only a small fraction of the time. Mostly, they take in jumbled images, words, smells, and sensations; then they extract meaning from the noise—a process that logicians call induction and lay people might call pattern recognition.

PS: Given your computer science background, and advocacy for formality in definition, I look forward to your entity, attribute analysis of the terms mode and state. As per IEEE Std 1016 or any other formalism you care to implement.

On Fri, 22 May 2026 at 20:05, Paulo Carvalho <paulovfc at gmail.com<mailto:paulovfc at gmail.com>> wrote:
Hello gents,

pardon my intromission, but I see the INCOSE Systems Engineering Handbook as a domain agnostic reference/guideline, and in that sense would see reasonable that text distinguishes between "state" and "mode" even if not providing a definitive definition for each.

Thus, leaving the user to define those terms for the particular /application/domain/system they are working on.

I could see a situation where a system has different operating modes (nominal, degraded, power-off, etc.) and each of these modes includes different internal states.
Cheers
Paulo



On Fri, May 22, 2026 at 10:19 AM Prof. Dr. Peter Bernard Ladkin <ladkin at causalis.com<mailto:ladkin at causalis.com>> wrote:
On 2026-05-22 01:27 , Les Chambers wrote:
>
> In these contexts, synonyms abominate the functional Safety countryside. They must be hunted down
> and eliminated with extreme prejudice - along with the “qualitative state machine(s)” they rode in
> on.
>
First, it seems silly to me to renounce synonyms. In the 61508 context, it would be ridiculous to
insist people say/write Equipment Under Control when they can write EUC and even more ridiculous to
insist they say/write Equipment Under Control Control System when they can say/write EUCCS.

Second, you seem to have a prejudice for working with numbers when it comes to state machines.
That's fine, I guess, as a personal preference. But if you perform any system development using
formal methods (which 61508 now says is "highly recommended" for any safety function) you will very
quickly have to get used to manipulating state machines which work on symbols which are not numbers.
For almost all formal verification techniques for the last 57 years use them or some equivalent.

PBL

Prof. Dr. Peter Bernard Ladkin
Causalis Limited/Causalis IngenieurGmbH, Bielefeld, Germany
Tel: +49 (0)521 3 29 31 00

_______________________________________________
The System Safety Mailing List
systemsafety at TechFak.Uni-Bielefeld.DE<mailto:systemsafety at TechFak.Uni-Bielefeld.DE>
Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
_______________________________________________
The System Safety Mailing List
systemsafety at TechFak.Uni-Bielefeld.DE
Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20260526/02440e11/attachment-0001.html>