Asynchronous Reactive Models – Event-based Analysis of Networks of Actors

[MUSIC] It’s my great pleasure to introduce Professor Marjan Sirjani to all of you She’s visiting here for the day She is a professor at Malardalen University in Sweden And her area of expertise is Programming languages and analysis techniques for network and distributed systems She has worked for many years on what we could call here domain-specific language, it’s called Rebeca For the kinds of systems that you see here in the title of our talk And today she’s going to present to us some of her work, and hopefully establish connections with all of you guys and for your future collaboration >> Yeah Thank you very much Thank you for having me here So yeah, I’m going to tell you about what we have been doing asynchronous reactive models and the analysis that we have been doing that is actual event based analysis of networks of actors So, this is my background You were asking, so now I’m in Sweden I’m also part timing in Reykjavik And I had many collaborators all over the world The Dutch people, and these are the actor community Carolyn [INAUDIBLE] and now Edward Lee And the model checking community, Crystal Olga and, okay So what I am going to say, the message of my talk is the Rebeca actor-based language, and how it is providing a usable and also analyzable model for distributed, concurrent, event-based asynchronous systems So you can call this domain, you can call it the domain specific But this is actually a very large domain so contains many applications And I will show you instead of I’m not going deep into theory that much today unless you ask me, I’m going to show you mostly the applications that use Rebeca And I show you how and why actors are friendly, and how they can be analyzed So our focus is on modeling of networks So they are asynchronous and event-based And they also deal with time and uncertainty So I don’t know How many years? Like for ten years we just had Rebeca and untimed version of it Something like what you have in P And we used it in many domains And then in 2008 we moved towards timed Rebeca and I will start showing timed Rebeca immediately, because I noticed that everyone is asking for time properties nowadays and also performance And then we added uncertainty and probabilistic models And recently we are moving towards adaptive systems The work we have done with Edward at Berkeley, it’s on adaptive systems, when you are dealing with change Something has changed, and you want to deal with the change And again, recently I’m working on the interface between cyber and physical, I still have to learn a lot in that domain And we want to mix this great and continuous work And for analysis, the focus has been on safety and performance We are now looking into security and privacy, but we haven’t done much on that So Actors, probably you know about Actors This is a reference model for concurrent computation And we have concurrent, distributed active objects They’re very much like what you have in P And it came from Hewitt as an agent-based language in MIT In eye lab And then Go, go introduced it as a concurrent object based language And people in SRI and others like Carolyn [INAUDIBLE] they made the formal basis and formal semantics for it So why I’ve not been in any of these groups So I didn’t inherit Actors as the language that they have to use We looked into different languages of process algebra, automata [INAUDIBLE] and other kind of modern languages I wanted to focus on concurrent distributed systems and also formal verification Bridging between these two have some kind of robust software in distribution

>> Can I ask you a question about this? I find that the research community is split between two kinds of people One of them calls it, the actor model, the other one calls it communicating state machines >> Communicating state machines, okay >> And again, how does bifurcation happen? They all seem to be roughly the same thing to me >> There’s another community that’s called concurrent objects >> Concurrent objects >> Objects, that’s a similar lab in Norway >> Okay >> So they are also as although may be even older than Actors >> Okay >> From 1960 something Yeah, concurrent state machines are, they are state machines Actors were functional in the beginning So they were [INAUDIBLE] actors, it was a functional language with no state variable So I made it, my version of Actors Rebeca is state-based I have variables because my target were programmers I wanted software engineers to work with my langauge. So- >> But even for the functional language, this date is still there, it’s just passed into the continuation, represented as the variable >> That’s true, but it’s not as intuitive as the- >> Definitely >> A program is, yeah >> I think another difference is the question of how to create or delete Actors, and if this is part of the model at all When you say communicating state machines there’s usually nothing in there but when these state machines get created or deleted While I think for actors- >> Or like the [INAUDIBLE] the creation, the [INAUDIBLE] typically don’t I see, okay >> And the way you write it, so you will see on the syntax of my language in a few minutes, few slides It’s just like Java State machines You have state machines, so like you’re working with SMB as a model checking person You have to write down your program in a state machines >> Nobody wants to actually write a state machine >> Exactly >> I see, so when people talk about state machines, they think about the actual thing you that you type, as opposed to the programming model >> I see >> Okay Some people if you start from your specification and they give you the spec as a state machine sometimes in some communities it’s like that then it’s okay to store it with state machines But programmers, software engineers think of a problem they write code They don’t write a state machine You know you? >> [INAUDIBLE] When you say state machine you think as a semantic >> [CROSSTALK] >> Which you could but you know that’s not going to be scalable by itself >> Yeah >> You have to use it in a principled way Okay sorry, sorry >> So that’s okay that’s nice to have conversation And by friendly I was telling you so I mean faithful and usable So yeah, I was talking of other modern language, I wanted my language to be object oriented, concurrent objects To I thought, okay, there’s a smaller semantic gap between the real world problems and my language then And I wanted to have construct for a synchronous modeling And for usability, I though object oriented, this is practitioner self engine you’d like it more than other type of programming or modeling And then I was hoping that this kind of actual language be analyzable because I was reading [INAUDIBLE] books and compositional verification And I was thinking okay, actors are isolated, they are really loosely coupled There’s no shared variables, there’s asynchronous communication, no wait They should be, there should be, that was my pHD thesis [INAUDIBLE], there should be nice composition or a verification approaches [INAUDIBLE] Enhancing [INAUDIBLE] reactive modules, they have to have some kind of conditions over shared variables I didn’t have that, so it turned out to be really nice You could invent compositional verification, nice compositional verification methods and other reduction techniques like symmetry partial Order all based on the model, at the level of the model We didn’t need to go to the level of the transition system for symmetry on partial order So it was also analyzable We were really happy about that and also in time [INAUDIBLE] because we focus on events Again, we could have very nice reduction techniques in analysis level, okay

And it proved to be a good choice because you guys are now using p So that’s my proof So where’s Rebeca? So this is the code but just- >> I have a question about the name Rebeca >> Yeah >> Why were [INAUDIBLE] >> Because it’s reactive object language, it’s not a name of >> It’s not a name >> It’s name of yeah, it was Alex in the beginning It was a live object language something like that but then my supervisor told me come on your objects are not really alive They are reactive, so we changed to Rebecca So it’s reactive object language And this is based on actor models, we have concurrent reactive objects And the syntax is Java, and we moved more and more and more I started from goals, actors, syntax, debate But my students pushed me through more and more Java like syntax It’s now all Java, the syntax, and the communication is just like actors A synchronous [INAUDIBLE], and in theory we have unbounded message cues for each [INAUDIBLE] [INAUDIBLE] is actor reactive object And for model checking, they put bounds on our queues of course There is no explicit receive so under computation it’s taking a message from top of the queue and executing it So we call it event driven So actors are just running, there is one thread of execution for each actor And then they’re doing whatever they have to do While they’re doing that or serving a message or event, they send messages to others They send, they’re not blocked, and they’re done with serving one message then looking to the queue and they take the other message, they run the server for that message >> Quick question, what’s the significance of taking the message from the top of the queue as opposed to any [INAUDIBLE] queue? >> You can have that In R2, they’re very implemented Now, its queue is FIFO But you can change the policy of taking your message from the queue >> So if the message delivery itself is facing deterministic and the q is not observable in any other way and getting a message out of it and it should matter right if the [INAUDIBLE] things are putting the q >> There we have this causality order so yeah, we have it, we have that, yeah >> Okay >> So if I send you a message and then another order, we keep the order >> You do, okay? >> And we have fairness, so it’s not lost >> Yeah, so Rebecca, the language also provides the mechanism to specify the [INAUDIBLE] policy So it doesn’t have to be first in, first out >> Right now it is first in first out But it’s very easy to change it to any kind of, especially now that we have time We are thinking of earliest deadline first or any other pattern matching like [INAUDIBLE] But we have never implemented that Right now the model taking too is FIFO, and- >> I think what she said to me that wasn’t the important bit is that you have fairness and causality >> Yes, we have that >> Even if you say I want something familiar in the queue you will still give stuff in order or not no? >> Say that again? Even if I what? >> Now you could, yeah, never mind, nothing >> If you want to have a network, which is faulty or whatever, you have to have an actor modeling that- >> Yes >> Network that is messing up with the order of messages >> Okay, and what back ends do you have for generic code? >> We have model checking tools that we do the model checking We check the assertions, we have CTL, ATL model checking >> But how do I execute the code I want to actually build an application >> Yeah, we have a very old Rebeca to Java tool, we haven’t use it but yesterday I called he said, I’m right on it So [LAUGH] cuz after reading [INAUDIBLE], I told him, you see that’s they’re advantage, they can just draw in their code, we need that But it’s very quick, now what we have, we get Rebeca, we map it to C++ code So it will be mapped to just C++ classes, and it’s just- >> Automatically, or by [INAUDIBLE]? >> Yeah, by our tool >> The tool is [INAUDIBLE] >> Yeah, the tool is doing that, for model checking, we have that But we never did the execution part of it So it needs some effort, but it’s not that much We will have it soon, I can promise

So if you’re thinking of running it on- >> [INAUDIBLE] >> NTL, you can write it in NTL You mean the properties recheck? What specifications do you mean? >> Well, so you can write NTL? >> We can write NTL >> But were you checking only safety properties or do you also check loudness properties? >> We can check loudness properties, yeah It can take [INAUDIBLE], we also have CTL model checking tool, but we never used it And now we have time CTL This one, we’re using it So this is very new and we are maintaining it >> So here’s what I don’t understand So the MPM property is stated outside, right? >> Yes, yes >> So how do you type check it? Are all of the fields of each rebec sort of like public? You’re gonna have to refer to those fields right, those state variables inside your LTL property >> Inside my LTL yes So Rebecs have their own state variables There is no shared variables but yes as a modeler as a specifier you can when you’re writing your specification you see everything So you can have Rebec one variable two equals green and Rebec three variable five equals red >> So we’re gonna create lots of instances of Rebec one >> Okay >> How do I refer to a particular instance >> You can refer to that, you have the name of your instance You can refer to that >> Okay >> The instance of the class >> So how are instances identified? >> I have to show you the code, like this So, here you have the reactive class, these are the classes, like Router and Core And here, you are instantiating r00, r01, c00, c01 so you have the instance names If you want to and dynamic active creation, do we have dynamic active creation? I think we had These are all very new We have dynamic topology So now we can pass names to other rebecs But I’m not sure if we can, that’s the really mess up our model taking tool if we create dynamically >> Yeah So that’s a huge difference with [CROSSTALK] >> That’s a- >> It goes in P- >> You have- >> Machine addresses are first-class values You can store them in variables You can boss them as cradled messages, so it’s very dynamic, the configuration of the network, the activity changes >> The configuration is dynamic now Now, this is the old Rebeca syntax It’s still valid, so you have your known rebecs here You say which router knows which one in the quotes statically, but now as you said they can pass the name of all the rebecs in as parameter So now you can change the configuration also But creation is different, I’m not sure if they have creation We have this model checking tool, we have to maintain that So we cannot have that many, any fancy feature that we add to the language, we have to support it in our model checking tool So now we have this change of configuration, but not yet dynamic- >> So you are saying the router r00 that’s the name of that particular router instance? >> Yeah, router is the class and this is instantiating r00 >> And then you pass r00 as an argument to the constructor of r01? >> Yeah, because these are the known rebecs Yeah this are the rebecs that r00 can see the routers that it can see The routers around it This is actually like this too The binding, the topology, the configuration of the network >> So that is roughly like creating a router and passing a reference- >> Yes, yes >> Here it’s interesting because I hear you did it only in the constructor and you can also do it in an explicit message sent? >> Yeah, that’s what I’m trying to say, yeah >> Okay >> Yeah, yeah So I call it dynamic topology Just passing the names of dynamic network topology That now, we have it But dynamic creations, so adding a router just at one time, we don’t have it yet >> That just did, right? I mean main is at runtime, when you’re executing main >> Yeah, but a new [INAUDIBLE] tier, like having new create- >> But how is it different? That’s just like new, right? >> For model checking, you under new I can add new there

But here, I have all my data structures there We have them, you know? >> Yeah, I think I know what you’re saying You’re saying that somehow the status of main is special >> Yes, I’m >> Main is like >> One, once at the beginning >> Okay, now I understand >> Yeah, so okay what I was telling you Yeah okay I’m done with this and now you see this one So here what I’m okay here is the class, the actor type, and it’s message server so you are just writing that These are like methods in object-oriented languages What else do I have? Yeah, asynchronous message sending So you’re sending giveAck message to your neighbor And this is your constructor And this is the body of a message server And you see we don’t have state machines, we have just code And here you have instances of different actors, and these are your the known rebecs here And you have other parameters, one is for example the, one of these is the So in theory, you don’t have, you have unbounded from model checking, you need to bound them Okay, so, yeah, Rebeca is used for model driven, do you have any question here? You’re fine now Yeah you will see more right there So it’s used for Model-Driven Development So in early stages of the design flow and also throughout the design process, you can have your Rebeca code It’s more abstract than a programming language And then you can explore the design space, and check safety, and properties also, properties and also performance So the, now we have performance, because we have Timed Rebecca And I will show you lots of examples, I hope So Timed Rebecca is an extension of Rebecca where we have computation time So you can write down what’s the delay, what’s the computation time for executing something You have the message delivery time which is the network delay So if you send a message to someone you can specify how long it takes to get to the other actor in the network And you can also have model periodic events and they key words for both of these are after and this one is delay And then you have message expiration or time out, so you put deadline When you send a message, I send a message to you, I put a deadline That means that that’s the, if your deadline is ten, it means you only have ten units of time to serve it After that, it expires >> What ten units of time? >> Whatever units of time, X units of time >> How do you measure time? >> It’s in model, it’s a modeling language So it’s like force case execution, you know? All those kinds of stuff >> Okay, okay I see >> It’s for a scheduling community >> So what you’re saying is that one unit of time elapsing and one rebec will also make one unit of time elapse in another rebec? It’s like the time model There’s global notion of time, and when time elapses, it elapses in all the rebecs at the same time >> Somehow, somehow What we say, just to be more elegant, we say we have synchronized local clocks Because actors are distributed, we all have our own local clocks and when we are doing model checking for Timed Rebeca we use that concept that I can just go ahead Regardless of what you are doing but we have that notion of global time So if like time stamps my message with ten, you also have ten >> It seem interesting, sorry, I can see like when more people build algorithms that it’s difficult to synchronize clocks and [INAUDIBLE] to rely on that but it’s very easy to rely on your local clock to your events somewhat predictably And a lot of things can be done just reading your own local clock A lot of algorithms work without you making any assumptions about the clock >> Sure >> Still but you wanna make assumptions on your own clock [INAUDIBLE] >> Yes but even that’s what I learned from Edward that now This distributed system

that the clocks can be so precise and synchronized, so you no more really worry about that that much Like in a car, if my time when the message to break is sent from some ECU to another ECU, the timestamp you can- >> I think it would not generalize that >> [CROSSTALK] >> It depends on time scales >> It depends on time scales >> The last time I talked to Edward at Berkeley he had recently read the Spanner paper and he was referring on that So, Spanner maybe Jay can tell us about it So, is Spanner making the assumption that is typically not made in distributor systems? >> Yeah >> It’s making an assumption about timing accuracy, not necessarily synchronized It’s not necessarily going to assume that if you send a message it will be received in a certain amount of time It’s if your clock says, it’s time T, it is within time T of true time >> T plus delta T, that’s what Google people were telling me yesterday, yeah, and they- >> It’s the anatomic clock, so >> Yeah, they were asking me about this and telling me- >> I think, I also wanted to talk about that Bill gave The algorithm, almost everything about your algorithm does not actually lag on that clock [INAUDIBLE] >> But actually, it does, it does rely on that maximum delta T That’s all this is about >> If we skip one part, it’s about how many that we’ve actually agreed on the database >> Yeah >> For that part there’s like one [INAUDIBLE] where it can be faster But the entire rest, for example, anything you write, is handled by two phase commit, which is accurate without any assumptions >> Okay, but this part that they’re doing is they’re counting on some maximum delta T delay, between all these distributed systems Am I right? That’s what I heard >> It depends on what you mean by delay [INAUDIBLE] >> The clock >> [INAUDIBLE] >> Yeah, yeah, the clock, sorry The clock, that’s what I meant So, the timestamp that you see after if you wait for delta T time, then you’re sure that you have received all the, right? Or no? >> You’re not sure you’ve received all of the messages, cuz the network could be arbitrarily, it’s the clock, if your clock says T then you know that it’s near T The real time is off by no more than >> And you know the maximum delay of the network too >> Well >> I think that’s what you’re really [INAUDIBLE] >> It could be network buffering, or [INAUDIBLE] >> Okay, so but that’s what >> [INAUDIBLE] >> That’s right [LAUGH] >> The most important part of these algorithms is that you can sort of, when you get, when you know what time somebody else has, you can sort of have a guarantee that their clock will advance predictably >> Okay >> You know the [INAUDIBLE] dates by certain time, [INAUDIBLE] clock also has [INAUDIBLE] that [INAUDIBLE], so you have sort of a lower [INAUDIBLE] on how far the clock goes forward I think that’s [INAUDIBLE] >> Okay, but that’s what Edward has in his [INAUDIBLE] then, he also rely on the- >> Founded network [INAUDIBLE] >> Yeah, that’s the idea Okay, so where are we? Okay, so this is the example, the network on chip example that I showed you a part of the code So, we have this network on chip We have all these routers and local cores, and we were working with our hardware group So, they were doing it in parallel Got all the specifications from them And they wanted to check, evaluate different routing algorithms One example was selecting the best place to put their memory in this network and chip, or choose buffer sizes And they were using Edge Spice, their assimilation tool And this was the ASPIN architecture, the two-dimensional mesh GALS NoC So, this ASPIN, they have XY routing algorithms So, if you want to dispatch the pack, send it here, this is how it moves first on the X, and then on the Y And there is also communication protocol, which is the four phase handshake communication protocol The channel is blocked until the packet arrives to the other router So, when you want to send a packet, you only have the input port, you only have four entries, so you send the neighbor give back, ask the neighbor for

some acknowledgement Receive the acknowledgment back Then you can send your packet And then, when the other packet comes to be routed the same way, because when this one is full you ask for an acknowledgement it doesn’t give you the acknowledgement until it dispatches the packet And then sends the acknowledgement, and you can then send the packet So, this is the four face handshake communication that they have I just explain it to show you how it’s smaller than Rebeca’s, so the exact same thing that you see in the network, you just write it down in the Rebeca call So, this is what I was telling you, the friendliness, the faithfulness of what you are modeling and the language that you have to model that So, this is what I showed you So, you have the routers and you have the course All that you see here and you have all these requests for send, get acknowledgement, give acknowledgement, and you instantiate your routers and course Okay, I should you this already And again, when you have this you will just write all these method servers, or methods in the body of your actor Okay? I’m just trying to show the one to one mapping How the model matches the real problem Right? Okay, and now about the time, so if you know that the computation is taking some time, you put this delay Somewhat most of the time modeling languages like the statements takes zero time, but then you have to model the time explicitly using this delay statement And this is that worst case execution that I mentioned They give you that, okay This computation is going to take two units of time, so you put delay two there And then, you know that sending a message to your neighbor is going to take three units of time So, you put three here And you put the time [INAUDIBLE] deadline on the message that you’re sending So, this is how you model it And if you want a kind of periodic event, you’re sending yourself a Every ten units of time So, you take it from you queue every ten minutes >> So, you cannot refer directly to your local clock? You can only refer to it indirectly using that keyword delayed on after >> Yes, yes Have this now statement, but then we took it away >> Interesting >> I mean, this is, I think this is very much like Apritis, except for the deadline phase But it’s today and after, I mean, those are realistic, I think >> What is the deadline? I didn’t understand the, that, the deadline six What does that mean? >> This is for a schedulability analysis So, actually, this has a different nature These are for modeling This is a kind of specification So, when I’m checking the schedulablity, I check the code, and tell you if any deadline is missed, you see? So I took the code, because many people are sending me many requests I just take them, execute them, take them, execute them And I have this deadline, and the moment any of these deadlines are missed, the model check here, come back to you and tell you okay, this one is missing So this is not schedulable It’s for task schedulability >> [INAUDIBLE] between the time that the action is enabled and when it completes? >> This the deadline between when I ask you to do something and you take it to do it Take the event to do it If you want any other kind of time difference you have to modulate somehow >> Can I ask you a question that’s a bit of a tease? >> I don’t know You ask I will decide if I want to answer or not [LAUGH] >> Since you have this all powerful temporal logic >> Mm-hm >> That you have available to you Why didn’t you just write the deadline in LTL? Why did you introduce extra syntax for it? >> Because people don’t like to write LTL and TCTL >> So then are you saying that you’re planning to dump LTL? >> No, but at least, for engineers who are only looking for schedulability, they can just breath and get rid of LTL and TCTL They really hate it Engineers hate it Are you really recording me? >> [LAUGH] I have one more question that’s a bit of tease >> Okay >> Once you get rid of LTL are you going to stop calling this model checking? >> I’m not going to get rid of it [LAUGH] You are saying that, I’m not saying that

We have TCTL You’re not going But we’d like you to use There is a sentence for it They let you to use what you want You pay for what you need Something like that There is some slogan for it >> Pay as you go >> Yeah Something like that Anyway, so if you don’t need TCTL, you can get rid of it, but if you need it, you will keep it of course We are in model checking community for god’s sake, so >> [LAUGH] >> Okay, so this is, yeah, communication delay, this is deadline for the receiver, and this is periodic text >> Sorry, originally, when you said deadline, I thought it had a model [INAUDIBLE] sense that after the deadline the messages are effectively removed from [INAUDIBLE] not that is necessarily an error It could just be that it has like an expiration time on it >> Yes, but you can continue but you get this warning >> Okay, warning so you can ignore the warning if you think it’s not an error >> Yes To be honest, I don’t know what our model checking is doing now but it’s easy to just do it Just go ahead and have a warning So that was schedulability analysis, and this is another way we can use our model So they had this NOC and they had this course here doing some stuff and they were thinking of putting memory here or here or here So they had three choices for memory placement and then we had special kind of scenarios of applications And when we did the evaluation first, we thought M2 is the best place, because it’s closest to all the cores Can you see that? If you just draw a graph, M2 is closest to all these cores But before there is a high congestion there it’s turned out that M1 is a better choice So when we did this kind of evaluation and yeah, and again okay, they could do that using their simulation tool but it took them 24 hours while it took us three seconds This is not a fair comparison probably because we have much less details, but this was a proof of concept that we showed that we are telling the right thing Even though we have much less details It’s an abstract model, we are telling the same thing that the is coming back Okay, yeah this is again showing that how the model NoC in TRebeca, that the one-to-one mapping of concepts in the real world and in Rebeca And to decide what to keep and what to abstract away it always depends on what you want to check So if you want to check the deadlock there are things that you have to keep, and the rest you can just abstract away Successful sending and receiving of packets and estimating the maximum end-to-end and packet latency Depending on what you want to check You decide on what to model Any questions here? You’re fine? Okay And then we have tool support We have model checking tool sets We check the deadlock, the queue size So because we have a bound in the queue, we may overflow, and we just come back telling you that we overflow So we can increase the bound and the queue You have assertion checks, and then you have schedulability analysis, CTL and LTL model checking And I should say, TCTL for their timed models And as I just told you briefly, we have, yeah This atomic execution of a method, I think you also have that in P, right? You don’t interleave when a message, when a service >> We only introduce interleaving that communication points >> Exactly, exactly We even don’t have that because the sensor are non-blocking We don’t even have that When we’re done we [INAUDIBLE] the other you know what I mean? So are non-blocking Are not the point of synchronization for us >> It gets tricky to even- >> We will have to discuss this over lunch >> Okay I know that in timed automata the phrase semantics we build for our language, time language was timed automata

And for that we need to model the queues explicitly and then since also became the point of synchronization And that’s why our state space is much more small Much smaller than timed automata, right? I hope I can get there to show you some of those kind theories stuff too Okay, I have to be quick So and yes, partial order symmetry and, yeah, and this is our tool It’s an Eclipse based tool And, yeah, these are some just and and stuff Okay, some sample projects and OCI showed you Network Protocols I wanna show you, Wireless Sensors Application or I have a lot to show you For NoC we check the routing and dispatching analysis I showed you also the memory placement for network protocols they are just kind of distributed protocols for that We are checking this kind of communication protocols We check the deadlock and loop foreedom For wireless and some applications it was task scheduling and track based traffic systems This is our new work on adaptiviness and change on the go and what we can- >> In the case of the wireless sensors application, what was the specification that they were worried about? What was the specification that you were checking? >> The configuration of their system, the number of sensors that they have to put Around the bridge for example And they had this frequency of checking And they have these delays or time that has to be spent by executing each task So we have parameters to play with and we came up with some kind of the best configuration >> No, I understand, but to do that, you have to ask those what if questions, right? >> Then what if is this schedulability >> The schedulability >> So there’s all the task so- >> The deadline thing that you were talking about >> The deadline thing that I was talking, exactly So we have, I will get there, we have these notes and then they had to, let me get to the slides This is, Fatemeh did this, I was not really involved in that, she is now an assistant professor in University of Tehran She worked on mobile ad hoc networks First, she was doing this using process algebra, then she switched to Rebecca And yeah, these are mobile ad hoc netoworks When they want to route a package from here to there, everything is changing, you don’t know which route is going to, people are moving around So you have to go forward and then come backward, send the signal go forward, then come back for it, establish the link and then send your packet You have this indirectly connected nodes, and the main problem in this kind of algorithms is that they may form some loops So that was what the other papers, I was grading them yesterday This is what people are checking, that the main safety properties, the loop freedom And she found that she checked the particle and she found loops And they tried to improve the protocol, the performance But then it turned out that they’re introducing this kind of loop generation >> So this is AOD report that you’re talking about, this is the Internet standard, right? >> Yes >> Is it buggy? >> It is buggy, and now they are in contact all the time So they also check, in version 13 and 16, they found loop is formed So they send them their spec, they check the specs So they are now in contact with people who are doing this stuff I don’t know if it’s working now or not >> Right, I was just curious the version that is currently implemented all over the world, what is- >> Probably hopefully they check it before releasing it So they are in contact with Fatehmeh, so they’re doing it I’m not involved in that but I know that they’re in contact and they’re checking this all the time And because the model is friendly it’s easy, it’s not, it’s easy to change it, it’s easy to- >> Who does the modeling? Who did the modeling in this? >> Fatemeh did it >> Not the AODD guy? >> No, they sent her the spec, they do the modeling Then she did the modeling, and she- >> Why don’t they do the modeling themselves? >> I don’t know, ask them

She knows the modeling language, I don’t know I was reading a paper, they are doing it using what, I know I’ve forgot The paper is still on my open tabs over Many people are doing that, finding books in this kind of protocols This is the wireless network you were asking, this is what we did with goal, and it is post-doc So they had this kind of sensors and the bridges, to find out if there’s an earthquake And they were doing it together with the engineering department And they were using simulation And of course the new actors very well So the post-doc could use, Rebecca, wrote the code in four hours, basically We wrote it together and we could find out it’s more precise than simulation, because we’ve searched the whole state space for certain scenarios of course So then he told us what are the scenarios then we can search the whole state space It more precise than simulation and we could find a better configuration So this are the parallel entities So you have the CPU sensor and radio within each node They are talking to each other And yeah, the CPU has to do a lot of work, and it shouldn’t miss the deadline That’s the schedulability that we check, okay? And we were checking different possible sampling rate and stuff I have to be a bit quick Stop me if I am too quick And then, we were comparing simulation, analytical approach, and model checking Analytical approach is too abstract, so they have to really assume that everything is periodic or aperiodic, or this or that But with Rebecca, you can just write whatever you want, the exact same thing that’s happening And so they are very much pessimistic in their analysis We are more realistic Simulation is very much like model checking, but this is the standard difference between simulation and model checking We are searching the complete state space Okay, and this is very new for me Now in Sweden, I’m working with Volvo Construction Equipment and Volvo cars but this is for this big machines in Volvo construction equipment So they have this electric side, they are making this car autonomous, and they’re using ROS So, it may be very much like what you guys are doing in DRO now So yeah, they are writing their ROS code and they are trying to model it using Rebecca and find out the possible problems So this is the summary So we did Verification of Network Protocols, Schedulability and Design Decisions for Distributed Real-Time Network Applications And I didn’t tell you about safety performance of track-based traffic control systems So we have an actor-family of languages to do all this stuff Shall I go ahead, shall I stop, shall I jump to the series called stuff? What shall I do? What’s my timing? >> An actor-family of language >> Don’t look at this one >> [LAUGH] >> Okay if you want you can >> No, no, no let’s keep going >> [LAUGH] That did take a lot of time So, I can tell you about track-based traffic control I can tell you about the theory of our time verification Which one do you want me to tell you and how much time? >> Track-based traffic control for me >> Okay, how much time do I have? >> You have, well, I think that you’ll have about five minutes We have been interrupting you quite a bit >> Five minutes? >> So five more minutes, yeah >> Okay, so this is another field of applications that we looked at, I was working with air traffic system control in Iceland I noticed that they have this tracks like in trains, and like in metros And also this is something I didn’t show you, like in smart hops that you can go from one place to another place using bus or bike or taxi or, these are smart city applications, and like in NOC So we’ve figured out this shared pattern between all

these applications So I call them track-based traffic control And then there is one difference, some of them, like the air traffic and the trains, they had a kind of centralized control While in these two there’s no centralized control, so this is just understanding the pattern of applications And then the project was not modeling and verifying these but handling the change So this is in the context of self-adaptive systems I wanted to know if there is a storm or something somewhere in the air How are we going to handle it? It’s not planning from the beginning So this is this kind of MAPE-K sensor monitor analyzed plan >> So you’re saying that the controlled algorithms, they’re somehow influenced by the sensors? >> Yes >> That are sensing weather pattern changes? >> Yes >> I see >> Yes >> And you wanted to see what changes happen as a result of that? You’re interested in asking what if questions about it? >> Yes, I sense the changes, so there is a storm over there, so now I have to change the routing of my airplane or the scheduling of my train Like if in a network, there is lots of traffic here, you want to reroute your packet on the fly, on the run This is self-adaptive kind of systems, okay? Like AI, this is where AI comes in AI is everywhere So and first we were thinking of actors of course, but the switch that each track is an actor and the moving objects are messages I think that was a very nice design pattern that they came up with >> The moving object >> Or messages >> The moving objects on the tracks you mean? >> Yeah, like airplanes, like trains Now there are like messages and the tracks or actors sending these messages to each other Do you see what I mean? We just, how you say that? >> I mean but what about the control algorithm? They would be actors too, right? >> It depends in a centralized control which is much easier, that’s how I started to work with Edward really Because he has this Ptolemy and they have this concept of directors, which are coordinators, which are centralized control If you have a centralized control, the coordinator knows everything about what event or for me, what airplane is where >> Okay >> That coordinator in Ptolemy, it knows everything, doesn’t know the details, but knows what is where So I can use that knowledge in that coordinator, and have different policies for changing the plan If it’s completely distributed, I have to do something else >> So who are you working with here, who owns this application, the Finland Air Space? >> Iceland >> Iceland Air Space? >> They are my use case I don’t know what you mean by the owner, but they are real world cases study that we are using They don’t own it, what do you mean? >> I mean, by owner I mean, there’s an artifact that you are modeling The real truth of that artifact lies with whom? >> Yeah, air traffic control systems >> Okay >> Yeah, it came from them Okay, yeah so this is where we came up with coordinated actors in Ptolemy for handling this change, and we have this concept of model@runtime And yeah, I think I should stop, right? >> Mm-hm, okay Yeah, that’s it, and- >> Anybody have any other questions? Actually, I have a comment about that last one I completely agree with you that this is very much in the spirit of AI, and asking questions on abstract models Because the reality is just so complicated that there’s no artifact that represents that you have to do modeling And it’s very interesting that you can ask these what if kind of questions here >> Yes >> And it’s, ultimately boils down to some kind of a search problem But here, it’s very interesting that the same search technology is being used ask what if questions about a completely

different application that’s got nothing to do with software verification at all >> Yes, that’s true >> It may be that there is an opportunity here, potentially a big opportunity >> I think so too, yeah >> I think that doing the big question is, who does the modeling? As long as doing the modelling, I think the size of the opportunity is going to be limited >> Yeah, when they were doing the modeling themselves? >> Yes, that’s why the opportunity can potentially become big >> And that’s why I chose a model which I think is usable So I think software engineers can write Rebaca really easily And here when you’re talking about verification, you’re right, it’s not that much verification So what we are trying to do is to find where the change happens and I call it magnifiers So I’d just focus on where the change is happening and find out, try to contain the change And see how we can stop the propagation of the change, its a kind of compositional verification, a mix of composition The interface between this block that change is happening inside it and the rest of the system It’s a mix of everything, this is a very nice project actually >> Cool >> Question for you So when you say, it is them that should do the modeling, what do you think would be the reason why they don’t do it? Is it because it’s too hard or is it because they are not serious enough about [CROSSTALK]? >> I think it’s a combination of things I think the opportunity is speculative, they don’t know that there is actually some, a pot of gold at the end of all this hard work The second thing is it’s hard, it requires both the wind specific knowledge and modeling and abstraction skills To me this is very reminiscencent of the situation five or six years ago before the phrase data scientists became vogue, right? So these days, these so-called data scientists, right, they are experts in statistical analysis but that by itself is not going to justify their existence They have become somewhat of an expert in a particular kind of domain so that they can quickly do that kind of modeling And ask questions and do fast iteration And I think that at this point, to believe that that kind of data analysis has enough value, there seems to be consensus I don’t think a similar consensus exists here >> Right >> Cool, thank you, thank you >> Thank you >> [APPLAUSE]