| Publication type: |
Article in Proceedings |
| Author: |
S. Autexier, D. Hutter, T. Mossakowski, A. Schairer |
| Editor: |
H. Kirchner, C. Reingeissen |
| Title: |
The Development Graph Manager MAYA (System description) |
| Book / Collection title: |
Algebraic Methodology and Software Technology, 2002 |
| Volume: |
2422 |
| Page(s): |
495 – 502 |
| Series: |
Lecture Notes in Computer Science |
| Year published: |
2002 |
| Publisher: |
Springer Verlag, London |
| Abstract: |
The use of formal methods is propagated to increase the security and safety of developed software. However, the logical formalization of software systems is error-proned. As even the verification of small-sized industrial developments require several person months, specification errors revealed in late verification phases pose an incalculable risk for the overall project costs. Thus, an evolutionary formal development approach is absolutely indispensable in all applications so far, as it was hardly ever the case that the development steps were correctly designed in the first attempt. The search for formally correct software and the corresponding proofs is more like a formal reflection of partial developments rather than just a way to assure and prove more or less evident facts. The MAYA-system supports an evolutionary formal development as it allows the user to specify and verify his/her development and maintain and reuse the verification work already done when changing the specification. MAYA supports the use of various (structured) specification languages like CASL and VSE-SL to formalize the software development. Moreover, MAYA provides a generic interface to plugin additional parsers for the support of other specification languages. |
| Internet: |
http://www.springerlink.com/(if5syuycp5cvx5nxgumd4c2a)/app/home/contribution.asp?referrer=parent&backto=searcharticlesresults,3,3; |
| PostScript Version: |
http://www.informatik.uni-bremen.de/~till/papers/maya.ps |
| Status: |
Reviewed |
| Last updated: |
04. 08. 2006 |
|
 |
