S

safety analysis 124–127

safety properties 123–126, 129, 147–148, 155, 156, 369, 382, 394

cruise control system 167–169

for mutual exclusion 126–127

safety violation 127, 130, 148

Savings Account Problem 105

Scott, K. 180

select 211

Selectable class 212, 217, 220, 226

selective receive 211–212

modeling and implementing 216–219

Selic, B. 180

SemaBuffer class 95, 99

semantic equivalences 394–395

Semaphore class 88

semaphore invariant 102

semaphores 86–93, 126, 127, 157

fixed bounded buffer using 100

in Java 89–93

modeling 86–93

send 209–211, 215

Sender class 212–214

SensorController class 302, 303, 305

sequential composition 320–321

set 374–375

set constant 67

set of action labels 16

Shah, D. 274

shared actions 41–45, 51, 59

shared objects 63–76

Shaw, M. 180, 274

shortest trace 108

signal and continue 103

signal and urgent wait 103

SimpleAllocator class 185, 186

SIMULA 104

Simulate 66

single-lane bridge problem 127–134

class diagram 130, 131

display using Bridge class 133

implementation 130–134

liveness 140–146

modeling 128–130

revised implementation 144–146

revised model 142–144

Sistla, A.P. 157

slave 202

Slave class 202, 204

sleep() 26, 30

Sloman, M.S. 274

SlotCanvas class 188, 212, 221, 228

Smaalders, B. 274

Smolka, S.A. 60

Space Invaders 306–315

applet display 307

implementation 313–315

modeling 307–312

safety analysis 311–312

speedup 265

SPIN 156

sprites 307–309

start() 26, 29, 30

starvation 134, 135, 185, 194, 208

state 11, 13, 15, 16, 24, 26

state machine 11, 12, 24, 31, 32

State Transition Diagrams (STD) 31

statecharts 31, 180, 181

STATEMATE 180

STOP 13, 22, 30, 108

stop() 21, 26, 30, 57

strong semantic equivalence 394

strongly connected component 138

structure diagram model 161

structure diagrams 50–52, 59, 60

Supervisor class 262, 263

supervisor-worker system 250–265

applet display 260, 261

class diagram 261

implementation 260–265

modeling 254–260

process architecture 250

safety analysis 257–260

SupervisorCanvas class 261, 262

Switch class 299, 302–304

SwitchControl interface 302

synchronized method 72, 73, 75, 77, 79, 84, 90, 95, 101

synchronous message passing 209–219

applet display 212, 213

definition 210, 232

in Java 212–214

modeling 214–215

synchronous model 39