Name
Abstract | ||
|---|---|---|
Abstractions are used in model checking to tackle problems like state space explosion or modeling of IO. The application of these abstractions in real software development processes, however, lacks engineering support. This is one reason why model checking is not widely used in practice yet and testing is still state of the art in falsification. We show how user-defined abstractions can be integrated into a Java PathFinder setting with tools like AspectJ or Javassist and discuss implications of remaining weaknesses of these tools. We believe that a principled engineering approach to designing and implementing abstractions will improve the applicability of model checking in practice. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1109/SCAM.2009.25 | Edmonton, AB |
Keywords | Field | DocType |
real software development process,principled engineering approach,engineering support,model checking,state space explosion,user-defined abstraction,engineering abstractions,java pathfinder setting,data mining,java,concrete,software development process,computational modeling,formal verification,testing | Programming language,Model checking,Computer science,Engineering support,Software,Software development process,AspectJ,Java,State space,Formal verification | Conference |
ISSN | ISBN | Citations |
1942-5430 | 978-0-7695-3793-1 | 3 |
PageRank | References | Authors |
0.50 | 12 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Michael Achenbach | 1 | 9 | 1.05 |
| Klaus Ostermann | 2 | 457 | 23.97 |