Author: Petermann U.

Source: Journal of Experimental & Theoretical Artificial Intelligence, Volume 12, Number 4, 1 October 2000 , pp. 489-498(10)

Publisher: Taylor and Francis Ltd

Abstract:

This case study describes the specification and formal verification of the key part of SPaS, a development tool for the design of open loop programmable control developed at the University of Applied Sciences in Leipzig. SPaS translates the high-level representation of an open loop programmable control into a machine executable instruction list. The produced instruction list has to exhibit the same behaviour as suggested by the high-level representation. We discuss the following features of the case study: characterization of the correctness requirements, design of a verification strategy, the correctness proof, and the relation to the Common Criteria evaluation standard.

Keywords: PROGRAMME; VERIFICATION; MODULAR; SPECIFICATION; INTERACTIVE; PROVING; PROGRAMMABLE; CONTROL

Language: English

Document Type: Research article

Affiliations: 1: Department of Computer Science , University of Applied Sciences Leipzig, P. O. B. 300066, D - 04251 Leipzig, Germany

Publication date: 2000-10-01

More about this publication?

• Editorial Board
• Information for Authors
• Subscribe to this Title
• ingentaconnect is not responsible for the content or availability of external websites

Related content

• In this: publication
• By this: publisher
• In this Subject: Computer Science
• By this author: Petermann U.

Website © Publishing Technology. Article copyright remains with the publisher, society or author(s) as specified within the article.

• Terms and conditions
• Privacy policy
• Information for advertisers