000 05030nam a22006255i 4500
001 978-3-540-48092-1
003 DE-He213
005 20240423132553.0
007 cr nn 008mamaa
008 121227s1999 gw | s |||| 0|eng d
020 _a9783540480921
_9978-3-540-48092-1
024 7 _a10.1007/3-540-48092-7
_2doi
050 4 _aQA75.5-76.95
072 7 _aUYA
_2bicssc
072 7 _aCOM014000
_2bisacsh
072 7 _aUYA
_2thema
082 0 4 _a004.0151
_223
245 1 0 _aCorrect System Design
_h[electronic resource] :
_bRecent Insights and Advances /
_cedited by Ernst-Rüdiger Olderog, Bernhard Steffen.
250 _a1st ed. 1999.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg :
_bImprint: Springer,
_c1999.
300 _aXIV, 422 p.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aLecture Notes in Computer Science,
_x1611-3349 ;
_v1710
505 0 _aMethodology -- Theories of programming: Top-Down and Bottom­up and Neeting in the Middle -- A Triptych Software Development Paradigm: Domain, Requirements and Software Towards a Nodel Development of a Decision Support System for Sustainable Development -- A Triptych Software Development Paradigm: Domain, Requirements and Software Towards a Nodel Development of a Decision Support System for Sustainable Development -- Real-Time Constraints Through the ProCoS Layers -- Real-Time Constraints Through the ProCoS Layers -- Monotonicity in Calculational Proofs -- Monotonicity in Calculational Proofs -- Programming -- The Alma Project, or How First-Order Logic Can Help us in Imperative Programming -- Type and Effect Systems -- Automation -- Proving Theorems About Java-Like Byte Code -- Multiple State and Single State Tableaux for Combining Local and Global Nodel Checking -- On the Existence of Network Invariants for Verifying Parameterized Systems -- Compilation -- Verification of Compilers -- Translation Validation: From SIGNAL to C -- Compilation and Synthesis for Real-Time Embedded Controllers -- Optimization Under the Perspective of Soundness, Completeness, and Reusability -- Application -- Verification of Automotive Control Units -- Correct Real-Time Software for Programmable Logic Controllers -- Formal Methods for the International Space Station ISS -- METAFrame in Practice: Design of Intelligent Network Services.
520 _aComputers are gaining more and more controle over systems that we use or rely on in our daily lives, privately as well as professionally. In safety-critical applications, as well as in others, it is of paramount importance that systems controled by a computer or computing systems themselves reliably behave in accordance with the specification and requirements, in other words: here correctness of the system, of its software and hardware is crucial. In order to cope with this callenge, software engineers and computer scientists need to understand the foundations of programming, how different formal theories are linked together, how compilers correctly translate high-level programs into machine code, and why transformations performed are justifiable. On the occasion of Hans Langmaack's retirement from his professorship and in order to honor his fundamental contributions to the field, the volume editors invited 17 internationally well known researchers to evaluate the state of the art in the area of correct system design. This book presents 17 mutually reviewed invited papers organized in sections on methodology, programming, automation, compilation, and application. It is a unique outline of what has been achieved in the area which dates back to a pioneering paper by Alan Turing in 1949.
650 0 _aComputer science.
650 0 _aCompilers (Computer programs).
650 0 _aComputers, Special purpose.
650 0 _aMachine theory.
650 0 _aArtificial intelligence.
650 1 4 _aTheory of Computation.
650 2 4 _aComputer Science Logic and Foundations of Programming.
650 2 4 _aCompilers and Interpreters.
650 2 4 _aSpecial Purpose and Application-Based Systems.
650 2 4 _aFormal Languages and Automata Theory.
650 2 4 _aArtificial Intelligence.
700 1 _aOlderog, Ernst-Rüdiger.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aSteffen, Bernhard.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
710 2 _aSpringerLink (Online service)
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783540666240
776 0 8 _iPrinted edition:
_z9783662172650
830 0 _aLecture Notes in Computer Science,
_x1611-3349 ;
_v1710
856 4 0 _uhttps://doi.org/10.1007/3-540-48092-7
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
912 _aZDB-2-BAE
942 _cSPRINGER
999 _c189239
_d189239