Welcome everyone. My name is Erotra. I'm glad my somewhat pretentious title has a lourd
you all inside. I hope not to disappoint. Hence the disclaimer that I have way too many
disclaimers to elaborate on. What is an operating system? I had to look it up on Wikipedia. I
did have some imagination of what it could be, having used one for a few years. But it
turns out, and it's slightly paraphrased because their definition is too long for me, it's a
software platform providing access to resources and services to run computer programs. Okay,
great. I knew that. That's what I use it for. Excellent. The title is about the universal
operating system. And universal to me would imply more generalisation. I've always felt that the
computer should evolve or computing should evolve. And I hope that we can move towards
freely sharing, using, combining, understanding whatever we do with the computer. And from my
personal perspective, from my day job, one aspect would be something about safety. And I've added
security, but I'm definitely not a security expert in all the automation that we may computers do
these days and hopefully in the near future. Because apparently we are dealing with a few
crises here and there. And I believe we have ideas to get those addressed using information
technology. I hope to learn from Jonathan at the level of representing information, how this
could be used in the future. But I'm sticking to this bit. I'm more operationally oriented,
so you could say, imperatively. And I know this is the declarative minimalist computing room. So
I'll try to bridge that. The ingredients that I hope that the future universal operating system
might incorporate is definitely the microkernel. Richard Stolman proposed for the GNU system a
few years back that it could have a microkernel. I would still love to see that happen. In the
community, work is being done on that. I hope to start to contribute to that. From a software
point of view, I believe everything should be modular. Small pieces because I'm just a human.
My head is limited and my understanding and time are short. Things should be definitely
decentralized. Client and server would be a natural way to go in the interaction between things. But
I want to focus on language semantics that might help us to move towards such a universal operating
system. Because I think if we add all of these ingredients, we're going to incur enormous complexities.
And I'm not really sure that if we go on in software development the way we do, it will actually
scale to the level that we need our information technology and our operating system to scale.
And I'm going to do that using a very silly example. This is actually the control of my
cruise controller in my car. The picture comes from the internet, of course.
I'm guessing most of you have heard about a cruise controller. Basically it's an
electronic device in a car and it runs a bit of software. But I want to use it as a metaphor to
talk to you about small modular things that can work in a larger environment with other small
modular things. And if you add and combine them enough complexity goes up and we need to figure
out a way to deal with that. So what is a cruise controller? I'm just going to read this out
because I haven't memorized this. Basically when it's not enabled, hence it's disabled,
the throttle, which is the thing under the hood that is normally controlled with your gas paddle,
is fully controlled by the driver if he or she pushes the gas paddle.
When it is enabled and you apply the set button, it captures the current velocity and uses that
to maintain that velocity over the course of time.
There are exceptions. In my car if I go uphill and I've set it at the lower limit,
it will drop down and just drop the cruise controller. And there are other reasons for it to
refer back to the human control instead of doing it automatically. One of them is if you press
the brake pedal or the clutch pedal, it has to stop because it would be very annoying if your car
continues moving while you don't want to. And of course as a human you can cancel it. Okay,
this is all really boring. But basically if we would put this declaratively, we just want the
damn thing to control our velocity. Done. Very abstractly. And I think this is a way in the future,
a declarative way to do that future automation.
But I've just been listing all of these pointless details which are still very abstract. If you
look at the car in greater detail, there's a lot of imperative stuff going on, stateful stuff.
And that's what we're trying to figure out a solution for. So we've been working on a language
which we call also pretentiously designed, spelled incorrectly.
Because if you look on the internet for the normal word design, you'll either find us. So
at least this alternate spelling helps search engines. The semantics of our language allow us to,
well, our language consists of interfaces and components basically. Interfaces are
behavioral specifications. So they record the protocol. I'll show you an example in a minute.
And these protocols are actually contracts of interaction between two components.
And our components are of course modular. So they are completely isolated from the world by
interfaces. And they are composable. You can stick them together and know that while they
maintain the protocol, therefore they can cooperate properly. We have a formal definition of our
semantics, meaning we actually express it in a formal process algebra. And I'll get back to that.
We can simulate our behavior at the interface level and the component level.
We can actually implement running code through code generation.
And we can actually automatically verify a bunch of aspects of interfaces and components. And
I'll try that to do that by example.
So let's start with an interface.
The pick. Sorry.
Something like this. The picture of the buttons on my steering wheel I showed you is
captured in terms of syntax here. There's the enable, disable button. The select, the current
velocity to be maintained. As a resume button or resume function, a cancel. And on the dashboard,
there's this LED that indicates that it's active or not.
But the human is expected to interact in a specific way with the rest of the car.
And that has been captured in this behavior bit. And our language takes a imperative approach.
So we define state. I just scrolled across that. So we have two state iterations and we
maintain that in variables, state and set point. And now we describe the interaction of the human
with the cruise controller in the car behaviorally. In other words, if the initial state is disabled,
we would accept an enable and become enabled. So dive into this further. I'll show you a picture
of what this could look like. Let's see. Sorry. So if I show you the state diagram
of the text I was just showing you, this is generated from that definition. This is what it
would look like. This slightly more human readable. And we have sort of an intuition for this, I think.
I'm going to make it slightly more complicated. Let's look at the
component, the cruise controller component itself. It is specified similarly. Almost there.
Yeah. We use the same language or the same concept. We define the behavior of the component
itself, but now it receives its messages through ports and the cruise controller is supposed to
interact with the different actors in the system, which is the human behind the human machine
interface, the pedals, the throttle, and we have a timer, which I will not go into.
I won't go through in all details through this behavior. I just want to show you the following.
Sorry. I have to give one more example. The thing that I really want to add,
which we have recently done, is an extension. Let me start over.
This is what it looks like in, this is the formal semantics of that behavior,
which we can actually feed to a model checker and check properties. And let me feed it to the model
checker. It checks all of our default properties and the user defined properties, which I will now
show you. So what we have just checked is that the component adheres to all of the interface
contracts and it actually adheres to the invariant predicates. One of the invariant predicates,
which is, you may have heard, there are cruise controllers who accelerate unwontantly. I have
tried to encode that in the state of the environment, which the cruise controller is trying to control.
And in this case, it would be, if the human has not activated the cruise controller,
it should never actively control the throttle. So that's recorded like this. And I can actually
make that fail by commenting out a throttle reset. And then that property will help us find a sequence
of events that would lead to this illegal behavior, this unwanted behavior. Okay, this was very detailed.
I'll try to wrap it up.
Oops. So I have to make the link to the universal operating system ahead. I want to foresee that
we will build a modular operating system. And because of the modularity and the distribution,
the cooperative complexity goes up. And I think we've figured out a way to leverage model checking
to help us there in the future. In the near future, trying to, I'm looking forward to adding that to
her development, engaged development. In the coming year, we already, we had already planned
to extend the scope of verification, including data contracts. But
if you want to know more, just come and find us online. Here are the details.
Excellent. Thank you.
So this system is GPL, it's out of the open.
Yes, you can find us on Savannah. It runs on gigs, a gigs install design.
Can you tell a little bit more about the automatic verification of the model?
Right.
That's the magic board.
Yes. We actually transform the model into MCRL2, which is a model calculus that allows you to do
specify formal properties and capture the formal behavior. So what we effectively do,
the execution semantics of the code that we generate is modeled in MCRL2. We verify the
entire state space of that code, which is more efficient than trying to test all the code.
And we have a composition guarantee.
So when it finds nothing wrong, that there is really nothing wrong. And it's not a matter of,
we didn't already have a time to find something at once.
Exactly. But there are always aspects that you cannot represent, which are also important.
You're welcome.
More questions?
Is it a result or possible outcome for the model? Does it commute to the whole solution space?
At the component level now.
You should repeat the question.
Sorry. Your question was to verify all of the properties, does it expand the entire solution
space? Exactly what we do at the component level. So the interfaces allow a certain behavior.
And you want to expand that entire behavior, synthesize that, and go through it and figure out
if there are any problems hiding there.
That's what we do.
Final question, is it used in production?
It's used in production. Oh, yes. Our biggest customer currently is a thermo-efficient scientific.
They make these huge electron microscopes. And I believe they've got about 1.2 million lines
of our code running.
Another question?
Yes. Thank you. Is it also possible to create distributed systems with design?
Currently, no. But I hope to integrate with what Christine will be talking about very soon.
And that will solve that bit.
Great. Thank you.