Name
Abstract | ||
|---|---|---|
Process models capture tasks performed by agents together with their control flow. Building and analyzing such models is important but difficult in certain areas such as safety-critical healthcare processes. Tool-supported techniques are needed to find and correct flaws in such processes. On another hand, event-based formalisms such as Labeled Transition Systems (LTS) prove effective for analyzing agent behaviors. The paper describes a blend of state-based and event-based techniques for analyzing task models involving decisions. The input models are specified as guarded high-level message sequence charts, a language allowing us to integrate material provided by stakeholders such as multi-agent scenarios, decision trees, and flowchart fragments. The input models are compiled into guarded LTS, where transition guards on fluents support the integration of state-based and event-based analysis. The techniques supported by our tool include model checking against process-specific properties, invariant generation, and the detection of incompleteness, unreachability, and undesirable non-determinism in process decisions. They are based on a trace semantics of process models, defined in terms of guarded LTS, which are in turn defined in terms of pure LTS. The techniques complement our previous palette for synthesizing behavior models from scenarios and goals. The paper also describes our preliminary experience in analyzing cancer treatment processes using these techniques. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1109/ICSE.2009.5070543 | Vancouver, BC |
Keywords | Field | DocType |
cancer,formal specification,medical computing,multi-agent systems,program diagnostics,program verification,programming language semantics,task analysis,behavior model synthesis,cancer treatment process,control flow,critical process model analysis,event-based technique,high-level message sequence chart,incompleteness detection,invariant generation,model checking,process model semantics trace,process-specific property,state-based technique,task model analysis,undesirable non determinism,unreachability detection | Model checking,Unified Modeling Language,Computer science,Control flow,Automaton,Process modeling,Real-time computing,Multi-agent system,Formal specification,Theoretical computer science,Rotation formalisms in three dimensions | Conference |
ISSN | ISBN | Citations |
0270-5257 | 978-1-4244-3453-4 | 16 |
PageRank | References | Authors |
0.97 | 13 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Christophe Damas | 1 | 196 | 9.08 |
| Bernard Lambeau | 2 | 197 | 9.79 |
| Francois Roucoux | 3 | 16 | 0.97 |
| Axel van Lamsweerde | 4 | 4059 | 347.79 |