ISSN:
1573-1383
Keywords:
computer-based real-time systems
;
safety-critical applications
;
requirements
;
systems architecture
;
specification
;
high-level timed programming
;
machine programming
;
hardware description
;
asynchronous circuits
;
correctness
;
duration calculus
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract PorCoS is the name of the ESPRIT project “Provably Correct Systems”. A system is seen as a technological system with embedded controlling processors, sensors, actuators, connecting channels and timers in a physical environment, especially a real-time or hybrid system with digital and continuous components. The goal of PorCoS is to contribute to mathematical foundation for analysis and synthesis and to mathematical principles, techniques and tools for systematic and correct design and construction of systems, especially in safety-critical applications. The article discusses the notion of system correctness and explains its non-absolute nature. Two forerunners of ProCoS are described, the so-called stack of Computational Logic Inc., Austin, Texas, and the three views of concurrent processes – nets, terms and formulas – of E.-R. Olderog. ProCoS is going beyond the forerunners and has extended the description levels: Requirements and systems architectural language, specification language, high-level programming language, machine language, hardware description language and description language for asynchronuous circuits. A major achievement of ProCoS is to have related the semantic models of several different system development levels and to have shown up how to mathematically prove correct the transitions between these levels w.r.t. the semantic relations. The Duration Calculus gives a basis for semantics and verification and crosses the boundary between discrete and continuous models. The lecture has been given at the Dagstuhl-Seminar “High Integrity Programmable Electronic Systems”, 27. 02. - 03. 03. 95, organized by W. J. Cullyer, W. A. Halang and B. J. Krämer.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1023/A:1007963427189
Permalink
