Abstract
The complexity of future systems level problems is driving the need for alternative approaches to examining the problem of architectural synthesis at higher levels of abstraction. In this paper we show how formal reasoning tools may be used to help address this complexity problem and allow the designer to explore the design space with impunity, thanks to the rigour afforded by the mathematical formalism, in the sure knowledge that the final design behaviour will satisfy the specification.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R.B. Hughes. Automatic Software Verification and Synthesis. In Proc. 2nd. Int. Conf. on Software Engineering for Real-Time Systems, pages 219–223. Institution of Electrical Engineers, September 1989.
E. Mayger and M. Fourman. Integration of formal methods with system design. In A. Halaas and P. B. Denyer, editors, VLSI 91, Edinburgh, Scotland, August 1991.
E. Mayger, M. Francis, R. Harris, G. Musgrave, and M. Fourman. The need for a core method. In EUROMICRO 91, September 1991.
R. B. Hughes, M. D. Francis, S. P. Finn, and G. Musgrave. Formal tools for tri-state design in busses. In Proceedings of the 1992 International Workshop on the HOL Theorem Prover and it Applications, Leuven, Belgium, September 1992.
D. Shepherd. The role of Occam in the design of the T800. Communicating Process Architecture, pages 93–103, 1988.
L. Paulson. Natural deduction proof as higher-order resolution. Logic Programming, 3:237–258, 1987.
M. Gordon. Why Higher-Order Logic is a good conclusion for specifying and verifying hardware. In G. Milne and P.A. Subrahmanyam, editors, Formal Aspects of VLSI Design. North-Holland, 1986.
F.K. Hanna and N. Daeche. Specifications and verification of digital systems using higher-order predicate logic. In IEE Proceedings, volume' 133, 1986. PtE No. 5.
Avra Cohn. A proof of correctness of the viper microprocessor: The first level. In Birtwistle and Subrahmanyam, editors, VLSI Specification, Verification and Synthesis. Kluwer Academic Publishers, 1988.
M. Fourman and E. Mayger. Formally based system design — interactive hardware scheduling. In G. Musgrave and U. Lauther, editors, VLSI 89, Munich, Germany, August 1989. Elsevier Science Publishers.
R.B. Hughes and R.M. Zimmer. Automated interactive verification of functional programming languages. In C.M.I. Rattray and R.G. Clark, editors, The Unified Computation Laboratory, pages 411–423. Oxford University Press, May 1992.
R. B. Hughes. Automated Interactive Software Verification and Synthesis. PhD thesis, Department of Electrical Engineering and Electronics, Brunel University, Uxbridge, Middx, U.K., July 1992.
A. Antola and F. Distante. DFG: a graph based approach for algorithmic flow driven architechture synthesis. In Proc. of EUROMICRO 91, Vienna, Austria, September 1991.
R. B. Hughes and G. Musgrave. Design-flow graph partitioning. In Proceedings of the 1992 International Workshop on the HOL Theorem Prover and its Applications, Leuven, Belgium, September 1992.
R. Milner, M. Tofte, and R. Harper. The Definition of ML. The MIT Press, Cambridge, Massachusetts, 1990.
M.P. Fourman and Eleanor M. Mayger. Formally based systems design—Interactive hardware scheduling. In VLSI '89. North-Holland, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Musgrave, G., Finn, S., Francis, M., Harris, R., Hughes, R.B. (1994). Formal methods and their future. In: Pichler, F., Moreno Díaz, R. (eds) Computer Aided Systems Theory — EUROCAST '93. EUROCAST 1993. Lecture Notes in Computer Science, vol 763. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57601-0_49
Download citation
DOI: https://doi.org/10.1007/3-540-57601-0_49
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57601-3
Online ISBN: 978-3-540-48286-4
eBook Packages: Springer Book Archive