Trusted computing systems

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback
Take a look at the new version of this page: [ beta version ]. Tell us what you think.

Trusted computing systems: the ProCoS experience

Full text

Pdf (2.17 MB)

Source

International Conference on Software Engineering archive
Proceedings of the 14th international conference on Software engineering table of contents

Melbourne, Australia

Pages: 15 - 34

Year of Publication: 1992

ISBN:0-89791-504-6

Author

Dines Bjørner

Sponsors

IEEE-CS\TCSE : TC on Software Engineering
ACS :
IEA :
IREE :
SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 27, Citation Count: 0

Additional Information:

references index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/143062.143080 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Karl Johan Astrom , Bjorn Wittenmark, Adaptive Control, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1994
	2	J. Barwise and J. Perry. Situations ad Attitudes. MIT Press, Cambridge, Mass., USA, 1983, 1986.
	3	W. R. Bevier, Kit: A Study in Operating System Verification, IEEE Transactions on Software Engineering, v.15 n.11, p.1382-1396, November 1989 [doi>10.1109/32.41331]
	4	William R. Bevier, Kit and the short stack, Journal of Automated Reasoning, v.5 n.4, p.519-530, Dec. 1989
	5	William R. Bevier , Warren A. Hunt, Jr. , J. Strother Moore , William D. Young, An approach to systems verification, Journal of Automated Reasoning, v.5 n.4, p.411-428, Dec. 1989
	6	William R. Bevier , Jørgen F. Søgaard-Andersen, Mechanically Checked Proofs of Kernel Specification, Proceedings of the 3rd International Workshop on Computer Aided Verification, p.70-82, July 01-04, 1991
	7	John Billingsley, Controlling with Computers: Control Theory and Practical Digital Systems, McGraw-Hill, Inc., New York, NY, 1989
	8	Dines Bjo:.KC /rner, Project graphs and meta-programs. Towards a theory of software development, Proc. of the CRAI Workshop on Software Factories and Ada on System development and Ada, p.117-152, January 1987, Capri, Italy
	9	D Bjorner, Software development graphs: a unifying concept for software development?, Proc. of the sixth conference on Foundations of software technology and theoretical computer science, p.1-9, December 1986, New Delhi, India
	10	D. Bjorner. Software Engineering and Programming: Past-Present-Future. IPSJ: Inform. Proc. Soc. of Japan, 8(4):265-270, 1986.
	11	D. Bjorner, On the use of formal methods in software development, Proceedings of the 9th international conference on Software Engineering, p.17-29, March 1987, Monterey, California, United States
	12	D Bjorner, The stepwise development of software development graphs: meta-programming VDM developments, VDM-Europe Symposium 1987 on VDM '87: VDM---a formal method at work, p.77-96, January 1987, Brussels, Belgium
	13	D. Bjorner. Annex 1, Technical Annex for ESPRIT Basic Research Action 3104: ProCoS (Provably Correct Systems). Technical report, Dept. of Computer Science, Technical University of Denmark, April 3 1989.
	14	D. Bjorner. A ProCoS Project Description. Published in two slightly difFerent versions: (1) EATCS Bulletin, October 1989, (2) (Ed. Ivan Pknder:) Proceedings: Intl. Conf on AI & Robotics, Strebske Pleso, Slovakia, Nov. 5-9, 1989, North-Holland, Publ., Dept. of Computer Science, Technical University of Denmark, October 1989.
	15	D. Bjorner. Draft Final Report ProCoS - ESPRIT BRA 3104. Technical report, Dept. of Computer Science, Technical University of Denmark, 3 February 1992.
	16	D. Bjorner. Software Development. Volume 1: Specification Principles - the VDM Approach. Lecture Notes, Department of Computer Science, Technical University of Denmark, 710 pages, 1992.
	17	D. Bjorner. Software Development. Volume II: Design Principles - the VDM Approach. Lecture Notes, Department of Computer Science, Technical University of Denmark, 599 pages, Incomplete, 1992.
	18	D. Bjorner , L. Druffel, Position statement: ICSE-12 Workshop on Industrial Experience Using Formal Methods, Proceedings of the 12th international conference on Software engineering, p.264-266, March 26-30, 1990, Nice, France
	19	D. Bjorner, A.E. Haxthausen, and K. Havelund. Formal Software Development Methods: From VDM to RAISE, and from ProCoS to LaCoS. In InfoJapan'90, Proceedings of IPSJ 30th Anniv. Conf. IPSJ, 2-5 October 1990.
	20	Dines Bjørner , Anne Elisabeth Haxthausen , Klaus Havelund, Formal, model-oriented software development methods: from VDM to ProCoS & from RAISE to LaCoS, Future Generation Computer Systems, v.7 n.2-3, p.111-138, April 1992 [doi>10.1016/0167-739X(92)90001-R]
	21	VDM-Europe Symposium 1987 on VDM '87: VDM---a formal method at work, January 1987
	22	D. Bjorner and M. Nielsen. Meta Programs and Project Graphs. In ETW: Esprit Technical Week, pages 479- 491. Elsevier, May 1985.
	23	Jonathan Bowen, Formal specification of the ProCoS/safemos instruction set, Microprocessors & Microsystems, v.14 n.10, p.631-643, Dec. 1990 [doi>10.1016/0141-9331(90)90038-W]
	24	Jonathan P. Bowen , Jifeng He , Paritosh K. Pandya, An Approach to Verifiable Compiling Specification and Prototyping, Proceedings of the 2nd International Workshop on Programming Language Implementation and Logic Programming, p.45-59, August 20-22, 1990
	25	S. Brock and C.W. George, The RAISE Method Manual. Technical Report LACOS/CRI/DOC/3, CRI: Computer Resources International, 1990.
	26	Zhou ChaoChen, M. R. Hansen, A. P. Ravn, and H. Rischel. A Requirements Definition Language. In preparation, 1992.
	27	Zhou Chaochen, C. A. R. Hoare, and A. P. Ravn, A Calculus of Durations. Information Proc. Letters, 40(5), 1992.
	28	A. M. Davis , P. A. Freeman, Guest Editors' Introduction: Requirements Engineering, IEEE Transactions on Software Engineering, v.17 n.3, p.210-211, March 1991
	29	JGanos Demetrovics , P. Rado , Elod Knuth, Computer-Aided Specification Techniques, World Scientific Publishing Co., Inc., River Edge, NJ, 1986
	30	Antoni Diner. Z: An Introduction to Formal Methods. Wiley, Chichester, UK, June 1990.
	31	R. C. Dorf, Modern Control Systems, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
	32	Anders P. Ravn (editor). Embedded, Real-time Computing Systems. ProCoS Monograph VOLI, 122 pages, Dept. of Computer Science, Technical University of Denmark, December 121991.
	33	H.H. Lovengreen (editor). Base System Verification. ProCoS Monograph VOl.IV, 137 pages, Dept. of Computer Science, Technical University of Denmark, December 12 1991.
	34	Gene F. Franklin , Michael L. Workman , Dave Powell, Digital Control of Dynamic Systems, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1997
	35	Asis Goswami , Michael Bell , Mathai Joseph, ISL: An Interval Logic for the Specification of Real-time Programs, Proceedings of the Second International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.1-20, January 08-10, 1992
	36	CORPORATE The RAISE Language Group, The RAISE specification language, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
	37	J. Guttag, J.J. Horning, and J.M. Wing. Larch in Five Easy Pieces. Technical Report 5, DEC SRC, Dig. Equipm. Corp. Syst. Res. Ctr., Palo Alto, California, USA, 1985.
	38	Kirsten M. Hansen , Anders P. Ravn , Hans Rischel, Specifying and verifying requirements of real-time systems, ACM SIGSOFT Software Engineering Notes, v.16 n.5, p.44-54, Dec. 1991
	39	Kirsten Mark Hansen. Designing a Lift Control System. Technical Report ProCoS, Dept. of Computer Science, Technical University of Denmark, February 1992.
	40	Kirsten Mark Hansen. Towards Program Specification, Verlag, ESPRIT BRA Series, 1992.
	41	Kirsten Mark Hansen. Towards Programs, volume {32}, chapter 4. Expected publ. by Springer Verlag, ESPRIT BRA Series, 1992.
	42	Kirsten Mark Hansen, Anders Peter Ravn, and Hans Rischel. Designing Verified Real-time Systems. Technial report, Dept. of Computer Science, Technical University of Denmark, Submitted for EuroMicro '92, Paris 28 Jan. 1992.
	43	Michael R. Hansen , Zhou Chaochen, Semantics and Completeness of Duration Calculus, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.209-225, June 03-07, 1991
	44	M.R. Hansen, Zhou ChaoChen, and J. Staunstrup. A Real-Time Duration Semantics for Circuits. Submitted to Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, March 1992, Princeton, NJ, USA, Dept. of Computer Science, Technical University of Denmark, 27 September 1991.
	45	M.R. Hansen, A.P. Ravn, H. Rischel, and Zhou ChaoChen. Duration Specifications for Shared Processors. School & Symposium: Formal Techniques in Real-Time and Fault-Tolerant Systems, January 1992, Nijmegen, The Netherlands, Dept. of Computer Science, Technical University of Denmark, October 1991.
	46	N.H. Hansen and E.V. Sorensen. On Risk Prediction for Repairable Safety-Critical Systems, a Theoretical Foundation. Technical report, Dept. of Computer Science, Technical University of Denmark, November 30 1990.
	47	David Harel, Biting the Silver Bullet: Toward a Brighter Future for System Development, Computer, v.25 n.1, p.8-20, January 1992 [doi>10.1109/2.161283]
	48	Ian Hayes, Specification case studies, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1987
	49	K .L. Heninger, Specifying Software for Complex Systems: New Techniques and their Application. IEEE Trans. Software Engineming, 6(1):2-13, January 1980.
	50	C.A.R. Hoare, He Jifeng, J. Bowen, and P. Pandya. An Algebraic Approach to Verifiable Compling Specification and Prototyping of the ProCoS Level O Programming Language. Presented at ESPRIT Conference, Brussels, Belgium, 12-15 November 1990. Kluwer Academic Publishers, pp 804-818., Programming Research Group, Oxford University Computing Laboratory, England, July 1990.
	51	Matthew S. Jaffe , Nancy G. Leveson , Mats P. E. Heimdahl , Bonnie E. Melhart, Software Requirements Analysis for Real-Time Process-Control Systems, IEEE Transactions on Software Engineering, v.17 n.3, p.241-258, March 1991 [doi>10.1109/32.75414]
	52	F Jahanian , A K Mok, Safety analysis of timing properties in real-time systems, IEEE Transactions on Software Engineering, v.12 n.9, p.890-904, Sept. 1986
	53	He JiFeng and Ernst-Riidiger Olderog (editors). Interfaces between Languages for Concurrent Systems. Pro- COS Monograph VOl.11,156 pages, PRG,, Oxford Univ., UK; and Inst. of Informatics, Oldenburg Univ., FRG, December 12, 1991.
	54	Cliff B. Jones, Systematic software development using VDM (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
	55	F.P. Brooks Jr. No Silver Bullet: Essence and Accidents of Software Engineering, In H.-J. Kugler, editor, Information Processing '86, pages 1069-1076. North- Holland Publ. Co., Amsterdam, The Netherlands, 1986. IFIP World Computer Congress.
	56	Warren A. Hunt, Jr., Microprocessor design verification, Journal of Automated Reasoning, v.5 n.4, p.429-460, Dec. 1989
	57	Ron Koymans, Specifying real-time properties with metric temporal logic, Real-Time Systems, v.2 n.4, p.255-299, Nov. 1990 [doi>10.1007/BF01995674]
	58	David Lightfoot. Formal specification using Z. Macmillan, 1991.
	59	Lennart Ljung, System identification: theory for the user, Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
	60	D.G. Luenberger. Introduction to Dynamic Systemts Theorg: Theory, Models - Applications. Wiley, 1979.
	61	R.E. Milne. The RSL Proof Rules. Technical Report LACOS/CRI/DOC/5, CRI: Computer Resources International, 1990.
	62	J. Strother Moore, A mechanically verified language implementation, Journal of Automated Reasoning, v.5 n.4, p.461-492, Dec. 1989
	63	J. Strother Moore, System verification, Journal of Automated Reasoning, v.5 n.4, p.409-410, Dec. 1989
	64	Mogens Nielsen , Klaus Havelund , Kim Ritter Wagner , Chris George, The RAISE language, methods and tools, Formal Aspects of Computing, v.1 n.1, p.85-114, Jan.-March 1989 [doi>10.1007/BF01887199]
	65	J. Nordahl. Design for Dependability. Technical report, Dept. of Computer Science, Technical University of Denmark, 30. Januar 1992.
	66	T. W. Olle, IFIP comparative review of information systems design methodologies: problem definition, Trends in information systems, North-Holland Publishing Co., Amsterdam, The Netherlands, 1986
	67	D L Parnas , P C Clements, A rational design process: How and why to fake it, IEEE Transactions on Software Engineering, v.12 n.2, p.251-257, Feb. 1986
	68	Amir Pnueli , Eyal Harel, Applications of temporal logic to the specification of real time systems (extended abstract), Proceedings of a Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.84-98, September 1988, Warwick, United Kingdom
	69	Ben Potter , Jane Sinclair , David Till, An introduction to formal specification and Z, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
	70	S Prehn, From VDM to RAISE, VDM-Europe Symposium 1987 on VDM '87: VDM---a formal method at work, p.141-150, January 1987, Brussels, Belgium
	71	A. P. Ravn and H. Rischel. Requirements Capture for Embedded Real-Time Systems. In Proceedings of IMA CS-MCTS '91 Symposium on Modelling and Control of Technological Systems, Villeneuve d'Ascq, France, May 7-10, 1991, volume 2, pages 147-152. IMACS, May 1991.
	72	Anders P. Ravn. Continuous Control, volume {32}, chapter 5. Expected publ. by Springer Verlag, ESPRIT BRA Series, 1992.
	73	Anders P. Ravn. Introduction, volume {32}, chapter 1. Expected publ. by Springer Verlag, ESPRIT BRA Series, 1992.
	74	A.P. Ravn, H. Riechel, and K.M. Hansen. Specifying and Verifying Requirements of Real-Time Systems. IEEE Trans. Software Engineering, 18, 1992.
	75	Hans Riechel. Specification and Design, volume {32}, chapter 2. Expected publ. by Springer Verlag, ESPRIT BRA Series, 1992.
	76	A. C. Shaw, Reasoning About Time in Higher-Level Language Software, IEEE Transactions on Software Engineering, v.15 n.7, p.875-889, July 1989 [doi>10.1109/32.29487]
	77	Jens U. Skakkebrek, Anders P. Ravn, Hans Rischel, and Zhou ChaoChen. Specification of Embedded, Realtime Systeme. Technical report, Dept. of Computer Science, Technical University of Denmark, EuroMicro Workshop on Formal Methods for Real-time Systems, 1992 December 1991.
	78	Jens Ulrik Skakkebrek. A Larger Case Study: Railway Crossing, volume {32}, chapter 7. Expected publ. by Springer Verlag, ESPRIT BRA Series, 1992.
	79	Jens Ulrik Skakkebrek. Development of Provably Correct Systems. Technical report, Dept. of Computer Science, Technical University of Denmark, 30 August 1991 M.Sc. Thesis.
	80	Jørgen F. Søgaard-Anderson , Camilla Østerberg Rump , Hans Henrik Løvengreen, A systematic kernel development, ACM SIGSOFT Software Engineering Notes, v.16 n.5, p.55-65, Dec. 1991
	81	E.V. Soensen. On the Specification of Dependability Requirements Involving Time Integration. Technical report, Dept. of Computer Science, Technical University of Denmark, October 12 1989.
	82	E.V. Sorensen. Brief Tutorial on Dependability Concepts. Technical report, Dept. of Computer Science, Technical University of Denmark, April 11990.
	83	E.V. Soensen. On Dependability Prediction of Safety Critical Systems. Technical report, Dept. of Computer Science, Technical University of Denmark, April 20 1990.
	84	E.V. Sorensen, N.H. Hansen, and J. Nordahl. From CSP Models to Markov Models: A Case Study. IEEE Trans. Software Engineering, 18, 1992.
	85	Erling Vagn Sørensen , Jens Nordahl , Niels Herman Hansen, From CSP Models to Markov Models, IEEE Transactions on Software Engineering, v.19 n.6, p.554-570, June 1993 [doi>10.1109/32.232021]
	86	E.V. Sorensen, J. Nordahl, and N.H. Hansen. Dependability, volume {32}, chapter 6. Expected publ. by Springer Verlag, ESPRIT BRA Series, 1992.
	87	J. M. Spivey, Understanding Z: a specification language and its formal semantics, Cambridge University Press, New York, NY, 1988
	88	J. M. Spivey, The Z notation: a reference manual, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
	89	Burghard v. Karger (editor). Compiler Development. ProCoS Monograph VO1.111,247 pages, Inst. of Informatics, CA Univ., Kiel, FRG, December 12 1991.
	90	J.C. Willems. Paradigms and Puzzles in the Theory of Dynamical Systems. IEEE Trans. on Automatic Control, 36(3):259-294, March 1991.
	91	Terry Winograd , Fernando Flores, Understanding computers and cognition, Ablex Publishing Corp., Norwood, NJ, 1986
	92	Jim Woodcock , Jim Davies, Using Z: specification, refinement, and proof, Prentice-Hall, Inc., Upper Saddle River, NJ, 1996
	93	Jim Woodcock , Martin Loomes, Software engineering mathematics, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
	94	William D. Young, A mechanically verified code generator, Journal of Automated Reasoning, v.5 n.4, p.493-518, Dec. 1989
	95	Zhiming Liu , Anders P. Ravn , Erlin V. Sorensen , Chaochen Zhou, A Probabilistic Duration Calculus, University of Warwick, Coventry, UK, 1992