Subscribe

Issue No.03 - March (2013 vol.39)

pp: 305-326

José N. Oliveira , University of Minho, Braga

Miguel A. Ferreira , Software Improvement Group, Amsterdam

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2012.15

ABSTRACT

Relational algebra offers to software engineering the same degree of conciseness and calculational power as linear algebra in other engineering disciplines. Binary relations play the role of matrices with similar emphasis on multiplication and transposition. This matches with Alloy's lemma “everything is a relation” and with the relational basis of the Algebra of Programming (AoP). Altogether, it provides a simple and coherent approach to checking and calculating programs from abstract models. In this paper, we put Alloy and the Algebra of Programming together in a case study originating from the Verifiable File System mini-challenge put forward by Joshi and Holzmann: verifying the refinement of an abstract file store model into a journaled (Flash) data model catering to wear leveling and recovery from power loss. Our approach relies on diagrams to graphically express typed assertions. It interweaves model checking (in Alloy) with calculational proofs in a way which offers the best of both worlds. This provides ample evidence of the positive impact in software verification of Alloy's focus on relations, complemented by induction-free proofs about data structures such as stores and lists.

INDEX TERMS

Metals, Software, Programming, Matrices, Calculus, Cognition, grand challenges in computing, Model checking, algebra of programming, software verification

CITATION

José N. Oliveira, Miguel A. Ferreira, "Alloy Meets the Algebra of Programming: A Case Study",

*IEEE Transactions on Software Engineering*, vol.39, no. 3, pp. 305-326, March 2013, doi:10.1109/TSE.2012.15REFERENCES

- [1]
Software Engineering: Report on a Conference Sponsored by the NATO SCIENCE COMMITTEE, Garmisch, Germany, Seventh to 11th October 1968, P. Naur and B. Randell, eds. Scientific Affairs Division, NATO, 1969.- [2] D.L. Parnas, "Really Rethinking 'Formal Methods',"
Computer, vol. 43, no. 1, pp. 28-34, Jan. 2010.- [3] R. Backhouse,
Mathematics of Program Construction, Univ. of Nottingham, 2004, draft of book in preparation. - [4] E. Kreyszig,
Advanced Engineering Mathematics, sixth ed. J. Wiley and Sons, 1988.- [5] R. Maddux, "The Origin of Relation Algebras in the Development and Axiomatization of the Calculus of Relations,"
Studia Logica, vol. 50, pp. 421-455, 1991.- [6] G. Schmidt,
Relational Mathematics, Encyclopedia of Mathematics and Its Applications. Cambridge Univ. Press, Nov. 2010.- [7] P. Freyd and A. Ščedrov,
Categories, Allegories, Mathematical Library, vol. 39. North-Holland, 1990.- [8] R. Bird and O. de Moor,
Algebra of Programming. Prentice-Hall, 1997.- [9] L. Barbosa and J. Oliveira, "Transposing Partial Components—An Exercise on Coalgebraic Refinement,"
Theoretical Computer Science, vol. 365, no. 1, pp. 2-22, 2006.- [10] L. Barbosa, J. Oliveira, and A. Silva, "Calculating Invariants as Coreflexive Bisimulations,"
Proc. 12th Int'l Conf. Algebraic Methodology and Software Technology, pp. 83-99, 2008.- [11] J. Oliveira and C. Rodrigues, "Pointfree Factorization of Operation Refinement,"
Proc. 14th Int'l Conf. Formal Methods, pp. 236-251, 2006.- [12] J. Oliveira, "Transforming Data by Calculation,"
Proc. Generative and Transformational Techniques in Software Eng. II, pp. 134-195, 2008.- [13] S. Wang, L. Barbosa, and J. Oliveira, "A Relational Model for Confined Separation Logic,"
Proc. IFIP/IEEE Second Int'l Symp. Theoretical Aspects of Software Eng., pp. 263-270, 2008.- [14] J. Oliveira, "Extended Static Checking by Calculation using the Pointfree Transform,"
Proc. LerNet ALFA Summer School Conf., pp. 195-251, 2008.- [15] J. Oliveira, "Pointfree Foundations for (Generic) Lossless Decomposition," Technical Report TR-HASLab:3:2011, HASLab, Univ. of Minho and INESC TEC, 2011.
- [16] R. Joshi and G.J. Holzmann, "A Mini Challenge: Build a Verifiable Filesystem,"
Proc. Verified Software: Theories, Tools, Experiments Conf., pp. 49-56, 2005.- [17] M.A. Ferreira and J. Oliveira, "An Integrated Formal Methods Tool-Chain and Its Application to Verifying a File System Model,"
Formal Methods: Foundations and Applications, vol. 5902, pp. 153-169, Springer, 2009.- [18] D. Jackson,
Software Abstractions: Logic, Language, and Analysis, revised ed. MIT Press, 2012.- [19] R. Backhouse,
Program Construction: Calculating Implementations from Specifications. John Wiley and Sons, Inc., 2003.- [20] S. Feferman, "Tarski's Influence on Computer Science,"
Logical Methods in Computer Science, vol. 2, pp. 1-1-13, 2006.- [21] S. Givant, "The Calculus of Relations as a Foundation for Mathematics,"
J. Automated Reasoning, vol. 37, no. 4, pp. 277-322, 2006.- [22] A. Tarski and S. Givant,
A Formalization of Set Theory without Variables. Am. Math. Soc., 1987.- [23] J. Backus, "Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs,"
Comm. ACM, vol. 21, no. 8, pp. 613-639, Aug. 1978.- [24] M.F. Frias, C.L. Pombo, and M.M. Moscato, "Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications,"
Proc. 13th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 587-601, 2007.- [25] N. Macedo, "Translating Alloy Specifications to the Point-Free Style," master's thesis, Univ. of Minho, 2010.
- [26] C. Jones,
Systematic Software Development Using VDM, second ed. Prentice-Hall, 1990.- [27] D. Méry, "Refinement-Based Guidelines for Algorithmic Systems,"
Int'l J. Software and Informatics, vol. 3, nos. 2/3, pp. 197-239, 2009.- [28] T. Hoare and J. Misra, "Verified Software: Theories, Tools, Experiments Vision of a Grand Challenge Project,"
Proc. Verified Software: Theories, Tools, Experiments Conf., pp. 1-18, 2005,- [29] C.B. Jones and J. Woodcock, "Editorial,"
Formal Aspects of Computing, vol. 20, no. 1,issue devoted to the Mondex grand-challenge in verified software, pp. 1-3, 2008.- [30] A. Schierl, G. Schellhorn, D. Haneberg, and W. Reif, "Abstract Specification of the UBIFS file System for Flash Memory,"
Proc. Second World Congress on Formal Methods, pp. 190-206, 2009.- [31] E. Kang and D. Jackson, "Designing and Analyzing a Flash File System with Alloy,"
Int'l J. Software and Informatics, vol. 3, no. 1, pp. 129-148, 2009.- [32] S. Owre, S. Rajan, J. Rushby, N. Shankar, and M. Srivas, "PVS: Combining Specification, Proof Checking, and Model Checking,"
Proc. Eighth Int'l Conf. Computer Aided Verification, pp. 411-414, July/Aug. 1996.- [33] P. Dybjer, Q. Haiyan, and M. Takeyama, "Verifying Haskell Programs by Combining Testing and Proving,"
Proc. Third Int'l Conf. Quality Software, pp. 272-279, 2003.- [34] P. Höfner and G. Struth, "On Automating the Calculus of Relations,"
Proc. Fourth Int'l Joint Conf. Automated Reasoning, pp. 50-66, 2008.- [35] P. Matos and J. Marques-Silva, "Model Checking Event-B by Encoding into Alloy,"
J. Computing Research Repository, vol. arXiv:0805.3256v2, 2008.- [36] C. Bolton, "Using the Alloy Analyzer to Verify Data Refinement in Z,"
Electronic Notes in Theoretical Computer Science, vol. 137, no. 2, pp. 23-44, 2005.- [37] A. Galloway, G. Lüttgen, J. Mühlberg, and R. Siminiceanu, "Model-Checking the Linux Virtual File System,"
Proc. Int'l Conf. Verification, Model Checking, and Abstract Interpretation, pp. 74-88, 2009.- [38] J.T. Mühlberg and G. Lüttgen, "Verifying Compiled File System Code,"
Proc. Brazilian Symp. Formal Methods, pp. 306-320, 2009.- [39] J. Yang, P. Twohey, D. Engler, and M. Musuvathi, "Using Model Checking to Find Serious File System Errors,"
ACM Trans. Computer Systems, vol. 24, no. 4, pp. 393-423, 2006.- [40] A. Butterfield and A.Ó. Catháin, "Concurrent Models of Flash Memory Device Behaviour,"
Proc. Brazilian Symp. Formal Methods, pp. 70-83, 2009.- [41] A. Butterfield and J. Woodcock, "Formalising Flash Memory: First Steps,"
Proc. IEEE 12th Int'l Conf. Eng. Complex Computer Systems, pp. 251-260, 2007.- [42] K. Damchoom and M. Butler, "Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B,"
Proc. Brazilian Symp. Formal Methods, pp. 134-152, 2009.- [43] W. Hesselink and M. Lali, "Formalizing a Hierarchical File System,"
Electronic Notes in Theoretical Computer Science, vol. 259, pp. 67-85, 2009.- [44] L. Freitas, J. Woodcock, and Z. Fu, "POSIX File Store in Z/Eves: An Experiment in the Verified Software Repository,"
Science of Computer Programming, vol. 74, no. 4, pp. 238-257, 2009.- [45] C. Morgan and B. Sufrin, "Specification of the UNIX Filing System,"
IEEE Trans. Software Eng., vol. 10, no. 2, pp. 128-142, Mar. 1984.- [46] J. Kramer, "Is Abstraction the Key to Computing?"
Comm. ACM, vol. 50, no. 4, pp. 37-42, Apr. 2007.- [47] J.M. Wing, "Computational Thinking and Thinking about Computing,"
Philosophical Trans. Royal Soc. A, vol. 366, pp. 3717-3725, Oct. 2008.- [48] L. Russo,
The Forgotten Revolution: How Science Was Born in 300BC and Why It Had to Be Reborn. Springer-Verlag, Sept. 2003.- [49] J. Ferreira, A. Mendes, A. Cunha, C. Baquero, P. Silva, L. Barbosa, and J. Oliveira, "Logic Training through Algorithmic Problem Solving,"
Proc. Third Int'l Congress Conf. Tools for Teaching Logic, pp. 62-69, 2011.- [50] M. in Computer Science and Engineering, "Formal Methods in Software Engineering Course," http://mei.di.uminho.pt/?q=enmfes-uk, 30 ECTS, Univ. of Minho, 2011.
- [51] J. Oliveira, "Calculating with Pointfree Alloy," contributed talk to the IFIP WG 2.1 #64 Meeting, Apr. 2009.
- [52] C. Necco, J. Oliveira, and J. Visser, "Extended Static Checking by Strategic Rewriting of Pointfree Relational Expressions," Technical Report FAST:07.01, CCTC Research Centre, Univ. of Minho, 2007.
- [53] P.F. Silva and J.N. Oliveira, ""Galculator": Functional Prototype of a Galois-Connection Based Proof Assistant,"
Proc. 10th Int'l ACM SIGPLAN Conf. Principles and Practice of Declarative Programming, pp. 44-55, 2008. |