Hybrid Rebeca

Description

Hybrid Rebeca, is an extension of actor-based language Rebeca, to support modeling of cyber-physical systems. In this extension, physical actors are introduced as new computational entities to encapsulate the physical behaviors. To support various means of communication among the entities, network is explicitly modeled as a separate entity from actors. We derive hybrid automata as the basis for analysis of Hybrid Rebeca models. In this version, CAN network is defined as network model for communications of the actors. Actors can communicate with each other either through the CAN network or directly by wire.

Tools

We developed a tool which implements the core rules of Hybrid Rebeca. No parser is implemented in the current version of the tool, so the Rebeca models can’t directly be used with the tool. Rebeca models are mapped manually to an intermediate code, and the intermediate code is fed to our tool. The output of our tool is a hybrid automaton equivalent to the Hybrid Rebeca model in the format of SpaceEx. SpaceEx is a framework for verificationhybrid systems. Verification of the model can be done by giving the output file to the SpaceEx tool.

Case Studies

Water Tank: show download

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
physicalclass Tank {
    knownrebecs{}
    
    statevars{
        real amount; 
        float inFlowCap, outFlowCap, inRate, outRate;
    }
    
    msgsrv initial(foat amount_, float inFlowCap_, float outFlowCap_) {
        amount = amount_;
        inFlowCap = inFlowCap_;
        outFlowCap = outFlowCap_;
        setMode(NotEmpty);
    }
    
    msgsrv OpenOutput() {
        outRate = outFlowCap;
    }
    
    msgsrv CloseOutput(){
        outRate = 0;
    }
    
    msgsrv OpenInput() {
        inRate = inFlowCap;
    }
    
    msgsrv CloseInput() {
        inRate = 0;
    }
    
    mode NotEmpty {
        inv(amount >= 0) {
            amount' = inRate - outRate;
        }
        guard(amount == 0) {
            setmode(Empty);
        }
    }
    
    mode Empty {
        inv(amount==0) {
            amount' = inRate;
        }
        guard(amount>0)
            setmode(NotEmpty);
    }
}

physicalclass Sensor {
    knownrebecs { 
        Controller controller;
        Tank tank;
    }
    
    statevars {
        real timer;
    }
    
    msgsrv initial() {
        setmode(Active);
    }
    
    mode Active {
        inv(timer<=0.05) {
            timer' = 1;
        }
        guard(timer==0.05) {
            timer = 0;
            setmode(Active);
            controller.setTankAmount(tank.amount);
        }
    }
}

softwareclass Controller {
    knownrebecs { 
        Tank tank;
    }
    
    statevars {
        float tankAmount;
    }
    
    msgsrv initial() {
        tank.OpenOutput();
    }
    
    msgsrv setTankAmount(float amount) {
        tankAmount = amount;
    }
    
    msgsrv control() {
        if(tankAmount <= 20)
            tank.OpenInput();
        if(tankAmount >= 30)
            tank.CloseInput();
    }
}

physicalclass Clock {
    knownrebecs { 
        Controller controller;
    }
    
    statevars {
        real timer;
    }
    
    msgsrv initial() {
        setmode(Active);
    }
    
    mode Active {
        inv(timer<=0.1) {
            timer' = 1;
        }
        guard(timer==0.1) {
            timer = 0;
            setmode(Active);
            controller.control();
        }
    }
}

main {
    Tank tank ():(25,3,2);    
    Sensor sensor(@CAN controller,@Wire tank):();
    Controller controller (@CAN tank):();
    Clock clock(@Wire controller):();

    CAN {
        priorities {
            controller     tank.CloseInput                   1
            controller     tank.CloseOutput                  2
            controller     tank.OpenInput                    3
            controller     tank.OpenOutput                   4
            sensor         controller.setTankAmount          5
        }
        delays {
            controller     tank.CloseInput                   0.01
            controller     tank.CloseOutput                  0.01
            controller     tank.OpenInput                    0.01
            controller     tank.OpenOutput                   0.01
            sensor         controller.setTankAmount          0.01
            
        }
    }
}

Vending Machine: show download

Brake by Wire: show download

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
physicalclass Wheel {
    knownrebecs {WCtlr ctlr;}
    statevars {float trq; real spd; real t;}
    msgsrv initial(float spd_) {
        spd = spd_;
        setmode(Rolling);
    }
    msgsrv setTrq(float trq_) {
        trq = trq_;    
    }
    mode Rolling {
        inv(t <= 0.05) {
            t' = 1;
            spd' = -0.1-trq;
        }
        guard(t == 0.05) {
            t = 0;
            ctlr.setWspd(spd);
            if(spd > 0)
                setmode(Rolling);
        }
    }
}
    
softwareclass WCtlr {
    knownrebecs {Wheel w; BrakeCtlr bctlr;}
    statevars {int id; float wspd; float slprt;}
    msgsrv initial(int id_) {
        id = id_;
    }
    msgsrv setWspd(float wspd_) {
        wspd = wspd_;
        bctlr.setWspd(id,wspd);
    }
    msgsrv applyTrq(float reqTrq, float vspd) {
        if(vspd == 0)
            slprt = 0;
        else
            slprt = (vspd - wspd * WRAD)/vspd;
        if(slprt > 0.2)
            wheel.setTrq(0);
        else
            wheel.setTrq(reqTrq);
    }
}

physicalclass Brake {
    knownrebecs {BrakeCtlr bctlr;}
    statevars {real bprcnt; real t; float mxprcnt; float r}
    msgsrv initial(float bprcnt_, float mxprcnt_) {
        bprcnt = bprcnt_;
        mxprcnt = mxprcnt_;
        r = 1;
        setmode(Braking);
    }
    mode Braking {
        inv(t <= 0.05) {
            t' = 1;
            bprcnt' = r;
        }
        guard(t == 0.05) {
            t = 0;
            bctrl.setBprcnt(bprcnt);
            if(bprcnt>=mxprcnt)
                r = 0;
            setmode(Braking);
        }
    }
}

softwareclass BrakeCtlr {
    knownrebecs {WCtlr wctlrR;WCtlr wctlrL;}
    statevars {float wspdR;float wspdL;float bprcnt;float gtrq;float espd;}
    msgsrv control() {
        espd = (wspdR + wspdL)/2;
        gtrq = bprcnt;
        wctlrR.applyTrq(gtrq, espd);
        wctlrL.applyTrq(gtrq, espd);
    }
    // Setters for wspdR, wspdL and bprcnt
    ...
}

physicalclass Clock {
    knownrebecs {BrakeCtlr bctlr;}
    statevars {real t;}
    msgsrv initial() {
        setmode(Running)
    }
    mode Running() {
        inv(t <= 0.05) {
            t' = 1;
        }
        guard(t == 0.05) {
            t = 0;
            bctlr.control();
            setmode(Running);
        }
    }
}

main {
    Wheel wR (@Wire wctlrR):(1);
    Wheel wL (@Wire wctlrL):(1);
    WCtlr wctlrR (@Wire wR, @CAN bctlr):(0);
    WCtlr wctlrL (@Wire wL, @CAN bctlr):(1);
    BrakeCtlr bctlr (@CAN wctlrR, @CAN wctlrL):();
    Brake brake(@Wire bctlr):(60,65);
    Clock clock(@Wire bctlr):();
    
    CAN {
        priorities {
            bctlr     wctlrR.applyTrq      1;
            bctlr     wctlrL.applyTrq      2;
            wctlrR    bctlr.setWspd        3;
            wctlrL    bctlr.setWspd        4;
        }
        delays {
            bctlr     wctlrR.applyTrq      0.01;
            bctlr     wctlrL.applyTrq      0.01;
            wctlrR    bctlr.setWspd        0.01;
            wctlrL    bctlr.setWspd        0.01;
        }
    }
}

Complex Heater: show download

Project Members

Fatemeh Ghassemi (Principal Investigator)
Marjan Sirjani
Iman Jahandideh

Iman Jahandideh, Fatemeh Ghassemi, Marjan Sirjani: Hybrid Rebeca: Modeling and Analyzing of Cyber-Physical Systems, CyPhy, 2018
PDF

Hybrid Rebeca

Description

Tools

Case Studies

Project Members

Related Publications