Name
Abstract | ||
|---|---|---|
By integrating formal specification and formal verification into the design phase of a system development process, the correctness of the system can be ensured to a great extent. However, it is not sufficient for a self-optimizing system that needs to exchange its components safely and consistently over time. Therefore, this paper presents a comprehensive verification framework to guarantee the dependability of such a self-optimizing system at the design phase (off-line verification) as well as at the runtime phase (on-line verification). The proposed verification framework adopts AsmL as intermediate representation for the system specification and on-the-fly model checking technique for alleviating the state space explosion problem. The off and the on -line verifications are performed at (RT-UML) model level. The properties to be checked are expressed by RT-OCL where the underlying temporal logic is restricted to time-annotated ACTL/LTL formulae. In particular, the on-line verification is achieved by running the on-the-fly model checking interleaved with the execution of the checked system in a pipelined manner. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11562948_6 | Lecture Notes in Computer Science |
Keywords | Field | DocType |
system development process,system specification,comprehensive verification framework,line verification,proposed verification framework,self-optimizing system,off-line verification,design phase,formal verification,on-line verification,object oriented,modeling,dependability,state space,object constraint language,program analysis,unified modelling language,model checking,formal specification,intermediate representation,optimization,linear logic,temporal logic | Functional verification,Model checking,Computer science,Intelligent verification,Runtime verification,Verification,High-level verification,Software verification,Distributed computing,Formal verification | Conference |
ISBN | Citations | PageRank |
3-540-29209-8 | 1 | 0.37 |
References | Authors | |
20 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| yao zhao | 1 | 1 | 0.37 |
| Martin Kardos | 2 | 9 | 2.61 |
| Simon Oberthür | 3 | 39 | 5.90 |
| F. J. Rammig | 4 | 27 | 4.36 |