Bibliography

1
AADL := The SAE Architecture Analysis and Design Language (AADL) supports model-based embedded systems engineering. With its associated tools, AADL gives you the power to specify, analyze, and generate embedded real-time systems. An SAE standard, AADL has been developed by and for the avionics, aerospace, automotve, and robotics communities. http://www.aadl.info/

2
Abdulla, P.A.; Cerans, K.; Jonsson, B.; Yih-Kuen Tsay, General decidability theorems for infinite-state systems, In: Logic in Computer Science, 1996. LICS '96. Proceedings., Eleventh Annual IEEE Symposium on Date: 27-30 Jul 1996, Pages: 313 - 321

3
Aichernig, B.K.; Maibaum, T. (Eds.) Formal Methods at the Crossroads. From Panacaea to Foundational Support, LNCS 2757, Berlin: Springer, 2003

4
, Alexander, M.; Gardner, W.; (eds)Process Algebra for Parallel and Distributed Processing, Boca Raron et.al.: CRC Press, 2009

5
Alur, R.; Henzinger, T.A.; Kupferman, O. Alternating-time temporal logic, In: Journal of the ACM (JACM), Volume 49 , Issue 5 (September 2002), 672 - 713, 2002, ISSN:0004-5411

6
R. Alur, L.J. Jagadeesan, J.J. Kott, and J.E. Von Olnhausen Model-checking of real-time systems: a telecommunications application, In: Proceedings of the International Conference on Software Engineering, 1997

7
R. Alur, T.A. Henzinger, P.-H. Ho. Automatic symbolic verification of embedded systems, In: IEEE Trans. on Software Engineering 22(3):181-201, 1996

8
R. Alur, C. Coucoubetis, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, S. Yovine The algorithmic analysis of hybrid systems, In: Theoretical Computer Science 138:3-34, 1995 (a preliminary version appeared in Proc. Conf. on Analysis and Optimization of Systems: Discrete-event Systems, LNCIS 199, 1994)

9
Alur, R.; Henzinger, T.A. Real-Time System = Discrete System + Clock Variables, In: Theories and Experiences for Real-Time System Development, AMAST Series in Computing, pp. 1-30, 1994. (See online: http://www.cis.upenn.edu/~alur/pub.html)

10
R. Alur, L. Fix, T.A. Henzinger Event-clock automata: A determinizable class of timed automata, In: Proceedings of the Sixth Conference on Computer-Aided Verification, LNCS 818, pp. 11-13, 1994

11
R. Alur and T.A. Henzinger A really temporal logic, In: Journal of the ACM 41:181-204, 1994

12
R. Alur, C. Courcoubetis, T.A. Henzinger The observational power of clocks, In: Proceedings of the Fifth Conference on Concurrency Theory, LNCS 836, pp. 162-177, 1994.

13
Alur, R.; Dill, D.L. A Theory of Timed Automata, theoretical computer Science, 126(2): 183-235, 1994

14
Alur, R.; Henzinger, T.A.; Ho, P.-H. Automatic symbolic verification of embedded systems, In: Real-Time Systems Symposium, 1993., Proceedings, Date: 1-3 Dec 1993, Pages: 2 - 11

15
Alur, R. Model-checking in dense real-time, In: Information and computing, 1993.

16
Alur, R.; Courcoubetis, C.; Dill, D. Model checking for Real-Time Systems, In: Logic in Computer Science, 1990. LICS '90, Proceedings., Fifth Annual IEEE Symposium on, Date: 4-7 Jun 1990, Pages: 414 - 425

17
R. Alur, D. Dill Automata for modelling real time systems, In: Proceedings of ICALP'90, volume 443 of Lecture Notes in Computer Science. Springer, 1990

18
Arnold, A. Systémes de transitions finis et sémantique des processus communicantes, In: Collection Études et Recherches en Informatique, Paris. Masson, 1992

19
Arnold, A.; Brlek, S. Automatic Verification of Properties in Transition Systems, In: SOFTWARE-PRACTICE AND EXPERIENCE, VOL. 25(6),Pp.579-596,1995

20
Arnold, A.; Nivat, M. Comportements de processus, In: Actes du Colloque AFCET ``Les Mathématiques de l'Informatique'', Pp.35-68, 1982

21
Asarin, E.; Caspi, P.; Maler, O. A Kleene theorem for timed automata, In. Logic in Computer Science, 1997. LICS '97. Proceedings., 12th Annual IEEE Symposium on, Date: 29 Jun-2 Jul 1997, Pages: 160 - 171

22
ASSERT := ASSERT (Automated proof based System and Software Engineering for Real-Time ) is an integrated project (IP) co-sponsored by the European Commission under the Information Society Technology (IST) priority within the 6th Framework Programme (FP6). The project addresses the strategic objective of "Embedded Systems". http://www.assert-online.net/

23
Asteroth, A.; Baier, Chr. Theoretische Informatik. Eine Einfuehrung in Berechenbarkeit, Komplexitaet und formale Sprachen, Muenchen: Pearson Studium

24
Attie, P.C.; Arora, A.; E.A. Emerson Synthesis of fault-tolerant concurrent programs, In: ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 26 , Issue 1 (January 2004), 125 - 185, 2004, ISSN:0164-0925

25
Attie, P.C.; Emerson, E.A. Synthesis of concurrent programs for an atomic read/write model of computation, In: ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 23 , Issue 2 (March 2001), 187 - 242, ISSN:0164-0925

26
Audsley, N.; Conmy, P. M.; Crook-Dawkins, S. K.; Hawkins, R.: Safety Challenges for Model Driven Development. In Metamodelling for MDA; First International Workshop; York, UK, November 2003

27
Bahill, A.T.; Henderson, S.; Requirements Development, Verification, an Validation Exhibited in Famous Failures, In: Systems engineering, Vol.8, No.1, 2004, Wiley InterScience, www.interscience.wiley.com, DOI 10/1002/sys.20017

28
Baier, C.; Katoen, J-P.; Principles of Model checking, London - Cambridge (MA): The MIT Press, 2008

29
Balzer, W., Empirische Theorien: Modelle, Strukturen, Beispiele, Wiesbaden (Germany): Friedr.Vieweg & Sohn, 1982

30
Balzer, W.; Moulines, C. U.; Sneed, J. D., An Architectonic for Science, Dordrecht (NL): D.Reidel Publishing Company, 1987

31
Barnett, M., K.R.M. Leino, W. Schulte. "The Spec# Programming System: An Overview." Proceedings of Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS). Marseille: Springer Verlag, 2004.

32
Beckert, B.; Hoare, T.; Hahnle, R.; Smith, D.R.; Green, C.; Ranise, S.; Tinelli, C.; Ball, T.; Rajamani, S.K.; Intelligent Systems and Formal Methods in Software Engineering, in: Intelligent Systems, IEEE, Volume 21, Issue 6, Nov.-Dec. 2006 Page(s):71 - 81

33
BELLINI,P.; MATTOLINI, R.; NESI, P.; Temporal Logics for Real-Time System Specification, ACM Computing Surveys, Vol. 32, No. 1, March 2000, 12-42

34
Berard, B.; Bidoit, M.; Finkel, A., Systems and Software Verification. Model-Checking Techniques and Tools: Model-checking Techniques and Tools,Berlin: Springer, 2001, ( ISBN-10: 3540415238, ISBN-13: 978-3540415237)

35
Berka, K.; Kreiser, L.; Logiktexte. Kommentierte Auswahl zur Geschichte der modernen Logik., 2nd. corr. ed., Berlin: Akademieverlag, 1973

36
A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, Y. Zhu Symbolic model checking using SAT procedures instead of BDDs, DAC '99: Proceedings of the 36th annual ACM/IEEE Design Automation Conference Pages: 317 - 320 , 1999, ISBN:1-58133-109-7

37
Bitsch, F.: Safety Patterns - The Key to Formal Specification of Safety Requirements. In: Proceedings of the 20th International Conference on Computer Safety, Reliability and Security, Springer Verlag Berlin Heidelberg, Lecture Notes In Computer Science; Vol. 2187, 2001, p. 176

38
Boehm, B.: A Spiral Model for Software Development and Enhancement. Computer, vol. 21, no.5, May 1988

39
Boerger, E.; Graedel, E.; Gurevich,Y., The Classical Decision Problem, 1st ed. 1997, 2nd printing, Berlin: Springer, 2001, (ISBN: 978-3-540-42324-9)

40
L. Bolc; A. Szalas (eds.), Time and Logic: A Computational Approach, London: UCL Press, 1995

41
Bourbaki, N., Theorie Des Ensembles, Paris: Hermann, 1970

42
Bowen, J. (2005).This document contains some pointers to information on Formal Methods, useful for mathematically describing and reasoning about computer-based systems, available around the world on the World Wide Web (WWW). Formal methods are a fault avoidance technique that help in the reduction of errors introduced into a system, particularly at the earlier stages of design. They complement fault removal techniques like testing: http://vl.fmnet.info/

43
Bowen, J. (2006). This document contains some pointers to publications concerning formal methods, especially those that are online, which are available around the world on the World Wide Web.:http://vl.fmnet.info/pubs/

44
Bowen, J. (2006). Page about the Z Notation: http://vl.fmnet.info/z/

45
Brace, K.S.; Rudell, r.L.; Bryant, R.E. Efficient Implementation of a BDD Package, 27th ACM/IEEE Design Automation Conference.

46
Bryant, R.E. On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication, In: IEEE Transactions on Computers, Volume C-40, Issue 2, Date: Febr.1991, 205-213

47
Bryant, R.E. Graph-Based Algorithms for Boolean Function Manipulation, In: Transactions on Computers, Volume C-35, Issue 8, Date: Aug. 1986, Pages: 677 - 691

48
Bultan, T.; Gerber, R.; Pugh, W.; Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results, In: ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 21 , Issue 4 (July 1999), 747 - 789, 1999, ISSN:0164-0925

49
CASL:= the Common Algebraic Specification Language: http://www.cofi.info/CASL.html

50
Burch, J.R.; E.M.Clarke; K.L.Millan; D.L.Dill; Hwang, L.J Symbolic Model Checking: 10$ ^{20}$ States and Beyond, In: IEEE 1990

51
Carnap, R. Introduction to Semantics, Cambridge (MA): Harvard University Press, 1942 (3rd. ed. 1948).

52
Chang, C.C.; Keisler, H.J.; Model Theory, Amsterdam et.al: North Holland Publ.Company, 1973

53
Chomsky, N. Three models for the description of language, in: IRE Transactions on Information Theory (2): 113-124, 1956

54
Chomsky, N. Syntactic Structures, The Hague: Mouton, 1957; Reprint. Berlin and New York 1985.

55
Chomsky, N. On certain formal properties of grammars, Information and Control (2): 137-167, 1959

56
Chomsky, N. Schuetzenberger, M.P. The algebraic theory of context free languages, in Braffort, P.; Hirschberg, D.: Computer Programming and Formal Languages. Amsterdam: North Holland, 118-161, 1963

57
Chomsky, N. Formal properties of grammars, in: Handbook of Mathematical Psychology. Vol.2, New York. John wiley and sons, 1963,Pp.323 - 418.

58
Church, A. A note on the Entscheidungsproblem, in: Journal of Symbolic Logic, Vol 1 (1936) pp. 40-41. WITH: Correction to A note on the Entscheidungsproblem, ibid., pp. 101-2.

59
Church, A. Review of A. M. Turing. On computable numbers, with an application to the Entscheidungsproblem, in: Journal of Symbolic Logic, Vol 2 (1937) pp. 42-43

60
Clarke, E. M. , Jr.; Emerson, E.A.; Siflakis, J. Model Checking: Algorithmic Verification and Debugging, Communications of the ACM, vol.52, 11, 2009, 75-84

61
Clarke, E. M. , Jr.; Grumberg, O.; and Peled, D.A. , Model Checking, MIT Press, 1999, ( ISBN-10: 0262032708, ISBN-13: 978-0262032704)

62
E. M. Clarke, O. Grumberg, D.Long Model Checking, Research Report

63
E. M. Clarke, O. Grumberg Avoiding the state explosion problem in temporal logic model checking, In: Annual ACM Symposium on Principles of Distributed Computing, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, Vancouver, British Columbia, Canada, Pages: 294 - 303, 1987, ISBN:0-89791-239-4

64
E. M. Clarke, E. A. Emerson, A. P. Sistla Automatic verification of finite-state concurrent systems using temporal logic specifications, In: ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 8 , Issue 2 (April 1986), Pages: 244 - 263

65
E. M. Clarke, E. A. Emerson, A. P. Sistla Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach, In: Annual Symposium on Principles of Programming Languages, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, 117 - 126, 1983, ISBN:0-89791-090-7

66
Clarke, E.M.; Emerson, E. A. Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, In: Proc. Logics of programs workshop, Yorktown Heights, New York, May 1981, LNC, Vol. 131, Pp. 52 - 71, ISBN:3-540-11212-X, London: Springer-Verlag, 1981

67
COFI := the common Framework Initiative or algebraic specification and development: http://www.cofi.info/index.html

68
COFI Tools Page: http://www.cofi.info/Tools/index.html and http://www.cofi.info/Tools/Correction.html(Last visited oct-23, 2006)

69
Cooper, D. C. (1972). "Theorem Proving in Arithmetic without Multiplication". in B. Meltzer and D. Michie, eds., Machine Intelligence. Edinburgh University Press: 91-100.

70
Coryoth. Formal Specification. Actual Discussion of Practitioners: http://www.kuro5hin.org/story/2005/7/29/04553/9714(Last visited oct-23, 2006)

71
COTRE := The goal of the COTRE project is to define a pragmatic and equiped method of modeling and validation of real time software architectures. This method will combine formal and semi-formal approaches in an industrial process ensuring continuity and traceability from the architectural stage to the implementation stage on the hardware target. This will be proposed as a candidate to the evolution of the present standards of the domain : nbsp;not only HOOD (widely recognized by the European industrialists of real time software) and UML, but also the current work of standardization of architectura l languages leaded by SAE (AADL, standing for Avionics Architecture Description Language). http://www.laas.fr/COTRE/brindex.html

72
Courcoubetis, C.; Vardi, M.Y.; Wolper, P.; Reasoning about fair concurrent programs, In: Annual ACM Symposium on Theory of Computing, Proceedings of the eighteenth annual ACM symposium on Theory of computing, Berkeley, California, United States, 283 - 294, 1986, ISBN:0-89791-193-8

73
DAS, D.; CHAKRABARTI, P.P.; KUMAR, R.; Functional Veri?cation of Task Partitioning for Multiprocessor Embedded Systems, ACM Transactions on Design Automation of Electronic Systems, Vol. 12, No. 4, Article 44, 1-53, Pub. date: Sept. 2007.

74
Davis, M. Computability and Unsolvability, New York - Toronto - London: McGraw-Hill Book Company, Inc.,1958

75
Davis, M. (Ed.). (1965). The Undecidable. Basic Papers On Undecidable Propositions, Unsolvable Problems And Computable Functions. Hewlett (NY): Raven Press.

76
DEFENSE ACQUISITION UNIVERSITY PRESS, SYSTEMS ENGINEERING FUNDAMENTALS, SUPPLEMENTARY TEXT, FORT BELVOIR, VIRGINIA 22060-5565, JANUARY 2001

77
Diestel, R. (ed.) Directions in Infinite Graph Theory and Combinatorics. Topics in Discrete Mathematics 3, Publishere: Elsevier - North Holland, 1992, ISBN 0444894144

78
Diestel, R.. (2006). Graphentheorie.(3.Aufl.). Berlin-Heidelberg: Springer-Verlag.

79
Dieudonné, J. Geschichte der Mahematik 1700-1900. Ein Abriss, Braunschweig - Wiesbaden: Friedr.Viehweg & Sohn, 1985 (French Edition Paris: Hermann, 1978).

80
DO-178B: Software Considerations in Airborne Systems and Equipment Certification. Radio Technical Commission for Aeronautics (RTCA) Standard DO-178B/ED-12B, Dez. 1999.

81
Doeben-Henisch, G.; Bauer-Wersing, U.; Erasmus, L.; Schrader,U.; Wagner, W. Interdisciplinary Engineering of Intelligent Systems. Some Methodological Issues, Proceedings of the International Workshop Modelling Adaptive And Cognitive Systems (ADAPCOG 2008) as part of the Joint Conferences of SBIA'2008 (the 19th Brazilian Symposium on Artificial Intelligence); SBRN'2008 (the 10th Brazilian Symposium on Neural Networks); and JRI'2008 (the Intelligent Robotic Journey) at Salvador (Brazil) Oct-26 - Oct-30, 2008

82
Doeben-Henisch, G. Reconstructing Human Intelligence within Computational Sciences: An Introductory Essay, In: Loula, A.; Gudwin, R.; Queiroz, J.; Artificial Cognition Systems, Eds., Hershey - London: Idea Group Publishing, 2006, pp.106-139

83
Doeben-Henisch, G.: The Planet Earth Simulator Project - A Case Study in Computational Semiotics, In: Proceedings IEEE AFRICON2004 Conference, 2004, pp.417-422.

84
Doeben-Henisch, G.: Reducing Negative Complexity by a Semiotic System. In: Gudwin, R., & Queiroz, J., (eds). Semiotics and Intelligent Systems Development. Hershey et al: Idea Group Publishing, 2006, pp.330-342.

85
Deben-Henisch, G.; Wagner, M. Validation within Safety Critical Systems Engineering from a Computational Semiotics Point of View, In: IEEE Africon2007 Intern.Conference, Windhoek (Namibia), Sept.2007.

86
Dreben, B.; Goldfarb, W., Decision Problem. Solvable Classes of Quantificational Formulas,Reading (MA): Addison-Wesley Educational Publishers Inc.,U.S., 1979, ( ISBN-10: 020102540X, ISBN-13: 978-0201025408)

87
D'Silva, V.; Kroening, D.; Weissenbacher, G.; A Survey of Automated Techniques for Formal Software Verification, In: Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on Volume 27, Issue 7, July 2008 Page(s):1165 - 1178

88
Duffy, David A. (1991). Principles of Automated Theorem Proving. John Wiley & Sons.

89
Duttheillet, C.; Vernier-Mounier, I.; Illie, J.-M.; Poitrenaud, D.: State-Space-Based Methods and Model Checking. In: Girault, Claude; Valk, R"udiger (Eds.): Petri Nets for Systems Engineers. A Guide to Modeling, Verification, and Applications. Springer, Berlin - Heidelberg - New York, 2003, pp.201-275.

90
Ebert, Chr. (2005). Systematisches Requirements Management: Anforderungen ermitteln, spezifizieren, analysieren und verfolgen. Heidelberg: dpunkt

91
Ehrlich, Alwina: Model Driven Architecture fuer die Entwicklung sicherheitskritischer Systeme. Diploma Thesis, FH - Frankfurt am Main - University of Applied Sciences, 2007

92
Emerson, E.A. Temporal and Modal Logic, in: Van Leeuwen, J. (Ed.), Handbook of Theoretical Computer Science. Formal Models and Semantics. Vol.B, Amsterdam: Elsevier & Cambridge (MA): The MIT Press, 1990; Pp.995-1072

93
Emerson, E.A.; Srinivasan, J.; A decidable temporal logic to reason about many processes, In: Annual ACM Symposium on Principles of Distributed Computing, Proceedings of the ninth annual ACM symposium on Principles of distributed computing, 233 - 246, 1990, ISBN:0-89791-404-X

94
Emerson, E.A.; Jutla, C.S. Tree Automata. Mu Calculus and Determinacy, IEEE 1991

95
Emerson, E.E.; Halpern, J.Y. ``Sometimes'' and ``Not Never'' Revisited: On Branching versus Linear Time Temporal Logic, In: JACM 33(1): Pages 151-178, 1986

96
Emerson, E.A.; Lei, Chin-Laung Modalities for Model Checking: Branching Time Logic Strikes Back, In: Annual Symposium on Principles of Programming Languages archive, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, New Orleans, Louisiana, United States, Pages: 84 - 96, 1985, ISBN:0-89791-147-4

97
Enderton, H.B. (2000). A Mathematical Introduction to Logic.(2nd ed). Academic Press

98
Esparza, J.; Nielsen, M. Decidability Issues for Petri Nets, In: BRICS Report Series , RS948, ISSN 09090878, 1994, BRICS Department of Computer Science, University of Aarhus, Ny Munkegade, building 540, DK 8000 Aarhus C , Denmark

99
ESPRESSO := ESPRESSO project : Synchronous programming for the trusted component-based engineering of embedded and mission-critical systems: http://www.irisa.fr/espresso/welcome_english.html

100
Farwer, B. $ \omega$-Automata, In: Graedel, E.; Thomas, W.; Wilke,Th., (Eds.), Automata, Logics, and Infinite Games. A Guide to Current Research, Berlin: Springer, 2002, (ISBN: 978-3-540-00388-5), Pp.3-21

101
Fischer, M. J., and Michael O. Rabin ( 1974. "Super-Exponential Complexity of Presburger Arithmetic." Proceedings of the SIAM-AMS Symposium in Applied Mathematics Vol. 7: 27-41.

102
Fitting, Melvin (1996). First Order and Automated Theorem Proving, 2nd edition, Springer.

103
Fokkink, W. (2000). Introduction to Process Algebra. Berlin: Springer

104
Fu.X; Da.X.; Yu, Zh. Modeling Dynamic Software Architecture Based on pi-Net, Information and Communication Technologies, 2006. ICTTA '06. 2nd Volume 2, Date: 24-28 April 2006, Pages: 2861 - 2865

105
Fujita, M.; Fujisawa, H.; Kawato, N.; Evaluation and Improvements of Boolean Comparison Method Based on Binary Decision Diagrams, IEEE 1988

106
Frederiksen, Rune: Use of the Rational Unified Process for development of safety-related computer systems. Thesis, Hogskolen i Ostfold Avdeling for infomatikk og automatisering, 2002

107
Gabbay, D.M. (ed)(1994). What is a Logical System?. Oxford: Clarendon Press.

108
Gallier, Jean H. (1986). Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers.

109
Galton, A. P., The Logic of Aspect, Oxford: Clarendon Press, 1984

110
Galton, A. P., Temporal Logics and their Applications, London: Academic Press, 1987

111
Galton, A. P., Time and Change for AI, in: D. M. Gabbay, C. J. Hogger, and J. A. Robinson, Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 4, Oxford: Clarendon Press, 1995, Pp. 175-240

112
Goldblatt, R., Logics of Time and Computation, Center for the Study of Language and Information, CSLI Lecture Notes 7, 1987

113
Gandy, R. (1988). The Confluence of Ideas in 1936, In Herken, R. (Ed.). (1988). The Universal Turing Machine. A Half-Century Survey. Hamburg-Berlin: Kammerer & Unverzagt, pp.55-111.

114
Garey, M. R., & Johnson, D. S. (1979). Computers and Intractability. A Guide to the Theory of NP-Completeness. San Francisco: W.H.Freeman and Company.

115
GI/ACM-AK Requirements: List of References http://www.gi-muc-ak-req.de/doc/literatur.htm

116
Girault, C.; Valk, R. Petri Nets for Systems Engineering. A Guide to Modeling, Verification, and Applications, Berlin - Heidelberg - New York: Springer, 2003

117
Goedel,Kurt. (1931) Über formal unentscheidbare Saetze der Principia Mathematica und verwandter Systeme, I, Monatshefte fuer Mathematik und Physik 38: 173-98. Translated in Jean van Heijenoort, 1967. From Frege to Goedel: A Source Book on Mathematical Logic. Harvard University Press: 596-616.

118
Graedel, E.; Thomas, W.; Wilke,Th., (Eds.), Automata, Logics, and Infinite Games. A Guide to Current Research, Berlin:Springer, 2002, (ISBN: 978-3-540-00388-5)

119
Grumberg, O.; Long, David E. ; Model checking and modular verification, May 1994 , Transactions on Programming Languages and Systems (TOPLAS) , Volume 16 , Issue 3 (May 1994), Pages: 843 - 871, Year of Publication: 1994, ACM, ISSN:0164-0925

120
Haddad, S.: Introduction: Issues in Verification, In: Girault, Claude; Valk, R"udiger (Eds.): Petri Nets for Systems Engineers. A Guide to Modeling, Verification, and Applications. Springer, Berlin - Heidelberg - New York, 2003, pp.183-200.

121
Halin, R. Graphentheorie, Vol.1+2, Darmstadt: Wissenschaftliche Buchgesellschaft, 1980, 1981.

122
Heijenoort, J.van From Frege to G"odel. A sourcebook in mathematical logic, Cambridge (MA): harvard University Press., 1967

123
Heitmeyer, C.; Lynch, N. The generalized railroad crossing: a case study in formal verification of real-time systems, In: Real-Time Systems Symposium, 1994, Proceedings, Date: 7-9 Dec 1994, Pages: 120 - 131

124
Heljanko, K. (1997). Model Checking the Branching Time Temporal Logic CTL. Helsinki University of Technology. Series A. Research Report. ISBN 951-22-3603-6, 1997

125
Henzinger, T.A.; Nicollin, X.; Sifakis, J.; Yovine, S. Symbolic model checking for real-time systems, In: Logic in Computer Science, 1992. LICS '92., Proceedings of the Seventh Annual IEEE Symposium on Date: 22-25 Jun 1992, Pages: 394 - 406

126
Herken, R. (Ed.). The Universal Turing Machine. A Half-Century Survey, Hamburg-Berlin: Kammerer & Unverzagt, 1988

127
Herrmann, Debra S.: Software Safety and Reliability. IEEE Computer Society Press, Los Alamitos, CA, U.S.A., 1999

128
Hilbert, D., and Ackermann, W. (1928). Grundzuege der theoretischen Logik (Principles of Theoretical Logic). Springer-Verlag

129
Hilbert, D. & Bernays, P. (1968). Grundlagen der Mathematik I. (2nd ed.). Berlin-Heidelberg-New York: Springer Verlag.

130
Hinst, P. (1974). Logische Propaedeutik.Eine Einfuehrung in die deduktive Methodik und Logische Sprachanalyse. Muenchen: Fink Verlag

131
Hintikka, J. (Ed.). (1975). Rudolf Carnap, Logical Empiricist. Dordrecht - Boston: D.Reidel Publishing Company.

132
C. A. R. Hoare Communicating sequential processes, In: Communications of the ACM, Volume 21, Issue 8 (August 1978), 666 - 677, 1978, ISSN:0001-0782

133
Hodges, A. Alan Turing, Enigma, (2nd ed. 1994). Wien-New York: Springer Verlag, 1983.

134
Hodges, A. Alan Turing and the Turing Machine, in: Herken, R. (Ed.). The Universal Turing Machine. A Half-Century Survey, Hamburg-Berlin: Kammerer & Unverzagt, 1988, Pp. 3-15

135
Hodges, W. (2001). Logic. An introduction to Elementary Logic. Penguin Books.

136
Hood, C. & Wiebel, R. (2005). Optimieren von Requirements Management & Engineering mit dem HOOD Capability Model. Heidelberg: Springer

137
HOPCROFT, H.L.; ULLMAN, J.D. Introduction to Automata Theory, Languages, and Computation, Reading (MA): Addison-Wesley Publ.Company, 1979

138
Houberdon, Jean-Louis; Babau, Jean-Philippe: MDA for embedded systems dedicated to process control. In Workshop on Model Driven Architecture in the Specification, Implementation and Validation of Object-Oriented Embedded Systems (SIVOEES), 2003, San-Francisco, CA, U.S.A., October 2003

139
R. Huuck ; Y. Lakhnech; B. Lukoschus; L. Urbina; S. Engell; S. Kowalewski ; J. Preußig Integrating timed condition/event systems and timed automata for the verification of hybrid systems, In: Engineering of distributed control systems, Pages: 59 - 80 , 2001, ISBN:1-59033-102-8, Publisher: Nova Science Publishers, Inc. Commack, NY, USA

140
IEC 61508: Functional safety of electrical/electronic/programmable electronic safety-related systems. International Electrotechnical Commission, Geneva, Switzerland, http://www.iec.ch

141
International Council on Systems Engineering (INCOSE), A GUIDE FOR SYSTEM LIFE CYCLE PROCESSES AND ACTIVITIES, INCOSE SYSTEMS ENGINEERING HANDBOOK, ed.by Cecilia Haskins, INCOSE-TP-2003-002-03, version 3, June 2006

142
International Council on Systems Engineering (INCOSE), 'WHAT TO' GUIDE FOR ALL SE PRACTITIONERS, SYSTEMS ENGINEERING HANDBOOK A, INCOSE-TP-2003-016-02, Version 2a, 1 June 2004

143
INCOSE - Requirements Management (RM) Tools Survey site: http://www.paper-review.com/tools/rms/read.php

144
INCOSE - Some Standards for Systems Engineering: http://www.incose.org/practice/standardsupdate.aspx

145
INCOSE - Systems Engineering: http://www.incose.org/practice/whatissystemseng.aspx

146
ISO/IEC 15288, System Life Cycle Processes: http://www.15288.com/

147
Jacobson, I., Booch, G., Rumbaugh, J.: The Unified Software Development Process. Addison-Wesley, 1999

148
Jensen, K.(1992). Coloured Petri Nets, Vol. 1, EATCS Monographs on Theoretical Computer Science. Berlin: Springer

149
Kamp, J. A. W., Tense Logic and the Theory of Linear Order, Ph.D. thesis, University of California, Los Angeles, 1968

150
Kelly, T. P.: Arguing Safety - A Systematic Approach to Managing Safety Cases. Dphil Thesis, University of York, UK, 1999.

151
Kelly, T. P.; McDermid, J. A.: Safety Case Construction and Reuse using Patterns. In Proceedings of 16th International Conference on Computer Safety, Reliability and Security (SAFECOMP'97), September 1997, Springer

152
Kleene, S.C., Representation of events in nerve nets and finite automata, In: Shannon, C. E.; McCarthy,J.,(Eds.) Automata Studies, (AM-34) Annals of Mathematics Studies), Princeton (NJ): Princeton University Press, pp.3-41, 1956, (ISBN-10: 0691079161, ISBN-13: 978-0691079165)

153
Kleene, St.C. Introduction to Metamathematics, Groningen. Wolters-Noordhoff & Amsterdam: Noth-Holland Publishing company, 1952

154
Kleene, S.C., Representation of events in nerve nets and finite automata, RAND Corporation, 1951 /* An elementary exposition of the problems and results obtained during investigations in August, 1951, of the kinds of events any finite automation can respond to by assuming one of certain states */

155
Klir, G.J., Facets of Systems Science, New York - London: Plenum Press, 1991

156
Kneale, W., & Kneale, M. (1986). The Development of Logic. Oxford: Clarendon Press.

157
Kopetz, H.; Real-Time Systems. Design Principles for Distributed Embedded Applications, Boston - Dorfrecht - London: Kluwer Academic Publishers, 1997

158
Kos, K. (2006). Computational Tree Logic (CTL): http://wwwtcs.inf.tu-dresden.de/ hofmann/download/pss20060524.pdf

159
KOSARAJU, S.R. Decidability of reachability in vector addition systems, Proc.14th Ann.Symp.on Theory of Computing, Pp.267-281, 1982

160
Kowalewski, S.; Preussig, J.; Engell, S.; Huuck, R.; Lahknecht, Y.; Urbina, L Analyse zeitbewerteter Bedingungs/ereignis-Systeme mittels Echtzeitautomaten-Tools, In: Proceedings Fachtagung Entwurf Komplexer Automatisierungssysteme (EKA'97), Braunschweig, 22.-23.Mai 1997

161
Kripke, S. A Completeness Theorem in Modal Logic, in: Journal of Symbolic Logic 24(1):1-14, 1959

162
Kripke, S. The Undecidability of Monadic Modal Quantification Theory, in: Zeitschrift fÃ14r Mathematische Logik und Grundlagen der Mathematik 8:113-116, 1962

163
Kripke, S. Semantical Considerations in Modal Logic, in: Acta Philosophica Fennica 16:83-94, 1963

164
Kripke, S. Semantical Analysis of Modal Logic I: Normal Modal Propositional Calculi, in: Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 9:67-96, 1963

165
Kripke, S. Semantical Analysis of Intuitionistic Logic I, in: In Formal Systems and Recursive Functions, edited by M. Dummett and J. N. Crossley. Amsterdam: North-Holland Publishing Co.

166
Kripke, S. Semantical Analysis of Modal Logic II: Non-Normal Modal Propositional Calculi, in: In The Theory of Models, edited by J. W. Addison, L. Henkin and A. Tarski. Amsterdam: North-Holland Publishing Co., 1965

167
Kripke, S. Identity and Necessity, in: In Identity and Individuation, edited by M. K. Munitz. New York: New York University Press, 1971

168
Kripke, S. Naming and Necessity, in: In Semantics of Natural Language, edited by D. Davidson and G. Harman. Dordrecht; Boston: Reidel., 1972 /* Sets out the causal theory of reference */

169
Kripke, S. Outline of a Theory of Truth, in: Journal of Philosophy 72:690-716, 1975 /* Sets his theory of truth (against Alfred Tarski), where an object language can contain its own truth predicate */

170
Kripke, S. Speaker's Reference and Semantic Reference, in: Midwest Studies in Philosophy 2:255-276, 1977

171
Kripke, S. A Puzzle about Belief, in: In Meaning and Use, edited by A. Margalit. Dordrecht and Boston: Reidel, 1979

172
Kripke, S. Naming and Necessity, in: Cambridge, Mass.: Harvard University Press. ISBN 0-674-59845-8, 1980 (reprint from 1972)

173
Kripke, S. Wittgenstein on Rules and Private Language: an Elementary Exposition, in: Cambridge, Mass.: Harvard University Press. ISBN 0-674-95401-7, 1982 /* Sets out his interpretation of Wittgenstein aka Kripkenstein */

174
Kripke, S. Russell's Notion of Scope, in: Mind 114:1005-1037, 2005

175
Kröning, D.; Weissenbacher, G.; Model Checking: Bugs in C-Programmen finden. Drum prüfe. , in: iX, vol.5/2009, 159 - 162.

176
Kroger, F., Temporal Logic of Programs, Berlin: Springer-Verlag, 1987

177
Krumke, S.O.; Noltemeier, H. (2005), Graphentheoretische Konzepte und Algorithmen. Wiesbaden: B.G.Teubner Verlag

178
Kummer, O. (2001). Introduction to Petri Nets and Reference Nets. Sozionik Aktuell, 1: http://www.informatik.uni-hamburg.de/TGI/forschung/projekte/sozionik/journal/index.html

179
Kupferman, O.; Vardi, M.Y.; From Linear Time to Branching Time, In: Transactions on Computational Logic (TOCL) , Volume 6 Issue 2, Pages: 273 - 294, 2005

180
Kupferman, O.; Vardi, M.Y.; Wolper, P.; An automata-theoretic approach to branching-time model checking, Journal of the ACM (JACM), Volume 47 , Issue 2 (March 2000), Pages: 312 - 360 , 2000, ISSN:0004-5411

181
Lakovic, Z.; Mai, P.; Schenk C.; Ye, W.; Yue, Z., Ueber die Entstehung der endlichen Automaten oder 'Warum haben endliche Automaten keine Namen?', Berlin: Technische Universitaet, MS 1999 (URL: http://www.google.de/search?q=lakovic+Mai+Schenk+Entstehung+endlichen+automaten+1999&ie=utf-8&oe=utf-8&aq=t&rls=org.mozilla:en-US:official&client=firefox-a)

182
K. G. Larsen, P. Patterson, Y. Wang UPPAAL in a nutshell, In: Springer International Journal of Software Tools for Technology Transfer, 1, 1997

183
K. G. Larsen, P. Petterson, Y. Wang Compositional and symbolic model-checking of real-time systems, In: In Proceedings of the 16th Real-Time Systems Symposium, Pp. 76-87, IEEE Computer Society Press, 1995.

184
Leveson, Nancy G.: Safeware - System Safety and Computers. Addison Wesley, Boston, MA, 1995

185
Leveson, Nancy G.; Heimdahl, Mats P.E.; Reese, Jon Damon:Designing Specification Languages for Process Control Systems: Lessons Learned and Steps to the Future. In Software Engineering - ESEC/FSE'99: 7th European Software Engineering Conference, Held Jointly with the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering, Toulouse, France, September 1999. Proceedings

186
Loveland, Donald W. (1978). Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science Volume 6. North-Holland Publishing.

187
Ludwig, G. (1978a). Die Grundstrukturen einer physikalischen Theorie. Berlin - Heidelberg - New York: Springer. Mackintosh, N. J. (Ed.). (1994). Animal Learning and Cognition. Academic Press.

188
Lutz, Robyn R.: Software Engineering for Safety. A Roadmap. in The Future of Software Engineering, Anthony Finkelstein (Ed.), ACM Press 2000

189
Machi, H.; Tomita, K.; Hosono Ch.; The relative completeness of a version of CTL$ ^{*}$, In: CATS '05: Proceedings of the 2005 Australasian symposium on Theory of computing, Volume 41 , Pages: 81 - 85, 2005, ISBN ISSN:1445-1336 , 1-920682-23-6

190
Mäkelä M. (2003). EFFICIENT COMPUTER-AIDED VERIFICATION OF PARALLEL AND DISTRIBUTED SOFTWARE SYSTEMS. ISBN 951-22-6791-8 ISBN 951-22-6792-6 (PDF) ISSN 1457-7615. Research Reports 81. Helsinki University of Technology Laboratory for Theoretical Computer Science. P.O.Box 5400. E-mail: lab@tcs.hut.fi. ISBN 951-22-6791-8. ISBN 951-22-6792-6 (PDF). ISSN 1457-7615

191
Manna, Z.; Pnueli, A. The Temporal Logic of Reactive and Concurrent Systems. Specification, Berlin. Springer, 1992

192
Manna, Z.; Pnueli, A. Temporal Verification of Reactive Systems. Safety, Berlin: Springer, 1995 /* This book is part 2 continuing the book 1992-book */

193
Mateescu, A.; Salomaa, A. Aspects of Classical Language Theory, in: Rozenberg, G.; Salomaa, A. (Eds.) Handbook of Formal Languages. Vol.1. Word - Language - Grammar, Berli: Springer, 1997, Pp.175 - 251

194
Mayr,E.W. An Algorithm for the General Petri Net Reachability Problem , In: SIAM J. Comput. 13,3, Pp. 441-460, 1984

195
McCulloch,W.S.; Pitts, W., A logical calculus of the ideas immanent in nervous activity, In: Bull Math. Biophys., 5, 115-133, 1943

196
McMillan, K.L. Symbolic Model Checking, Boston - Dordrecht - London: Kluwer Academic Publishers, 1993

197
Mealy, G.H. A method for synthesizing sequential circuits, in: Bell System Technical Journal, 34(5):1045-1079, 1955

198
Medvidovic, N.; Taylor, R.N. (2000). A classification and comparison framework for software architecture description languages. Software Engineering, IEEE Transactions on, Volume 26, Issue 1, Date: Jan 2000, Pages: 70 - 93

199
MeMVaTEx := The objective of the MeMVaTEx project is to complete the model-based development process by a modeling methodology that supports the development contonuity, model refining and interoperability between heterogeneous modeling formalisms. http://www.memvatex.org/scripts/home/publigen/content/templates/show.asp?L=EN&P=55&vTicker=alleza

200
Minsky, M. L.Computation: Finite and Infinite Machines, Englewood Cliffs (NJ): Prentice Hall, Inc., 1967

201
Mittelstrass, J. (Ed.), Enzyklopaedie Philosophie und Wissenschaftstheorie, Vol. 1-4, Stuttgart - Weimar: Publisher J.B.Metzler, 1995-1996

202
ModelWare := MODELWARE is defining and developing the complete infrastructure required for large-scale deployment of MDD strategies and validating it in several business domains. The project combines innovations in modelling technologies, engineering processes and methodologies, tool development (both generic and domain specific), standardisation, experimentations and change management. The successful adoption of MDD is ensured through communities of tool providers, open source software contributors and end-users. In particular, MODELWARE launched the Eclipse MDDi project aimed at developing an open MDD platform www.eclipse.org/mddi. MODELWARE initiated and is supporting the annual European conference on MDD ECMDA-FA with the support of the OMG http://www.ecmda-fa.org/. http://www.modelware-ist.org/

203
Moldt, D.; Kordon, F.: Systems Engineering and Validation In: Girault, Claude; Valk, R"udiger (Eds.): Petri Nets for Systems Engineers. A Guide to Modeling, Verification, and Applications. Springer, Berlin - Heidelberg - New York, 2003, pp.405-415.

204
MOLL, R.M; ARBIB, M.A.; KFOURY, A.J.; PUSTEJOVSKY, J. An Introduction to Formal Language Theory, Berlin - New York: Springer Verlag, 1988

205
Moore, E.F., Gedanken-Experiments on Sequential Machines, In: Shannon, C. E.; McCarthy,J.,(Eds.) Automata Studies, (AM-34) Annals of Mathematics Studies), Princeton (NJ): Princeton University Press, pp.129-153, 1956, (ISBN-10: 0691079161, ISBN-13: 978-0691079165)

206
Morris, C.W., Symbolik und Realitaet, Mit einer Einleitung von Achim Eschbach. Frankfurt am Main: Suhrkamp Verlag, 1981

207
Morris, C.W., Pragmatische Semiotik und Handlungstheorie, Mit einer Einleitung von Achim Eschbach. Frankfurt am Main: Suhrkamp Verlag, 1977

208
Morris, C.W., Writings on the General Theory of Signs, The Hague - Paris: Mouton Publ.,1971

209
Morris, C.W., Signification and Significance. A Study of the Relations of Signsc and Values, Cambridge (MA): MIT Press,1964

210
Morris, C.W., Towards a Unified Theory of Human Behavior, New York: Prentice Hall Inc.,1956

211
Morris, C.W., Signs, Language and Behavior, New York: Prentice-Hall Inc., 1946 (2nd. ed. 1947)

212
Morris, C.W., Foundations of the Theory of Signs, Chicago: University of Chicago Press (repr. In (MORRIS 1971)), 1938

213
Morris, C.W., Logical Positivism, Pragmatism, and Scientific Empiricism, Paris: Hermann et Cie., 1937

214
Morris, C.W., Symbolik und Realitaet, (German translation 1981 of the unpublished dissertation of Morris by Achim ESCHBACH). Frankfurt: Suhrkamp Verlag, 1925

215
Mosses, P.D. Denotational Semantics, in: Leeuwen, J. van (ed), Handbook of Theoretical Computer Science, Vol.B, Formal Models and Semantics; (Amsterdam et.al: Elsevier) and (Cambridge (MA): The MIT Press), chap.11,1990.

216
Nain, S.; Vardi, M.Y. Branching vs. Linear Time: Semantical Perspective. Version 1.1, MS 2007, Rice University, Dept. of Computer Science, Houston, TX 77005-1892, USA (URL: http://www.cs.rice.edu/ vardi/papers/ )

217
Nebut, C.; Fleurey, F.; Traon, Y.L.; Automatic Test Generation: A Use Case Driven Approach, in: IEEE Transactions on Software Engineering, Vol.32, No.3, March 2006, Pp.140 - 155

218
Nelson, G. & Oppen, D. C. (Apr. 1978). "A simplifier based on efficient decision algorithms". Proc. 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages: 141?150.

219
Neptun := (Nice Environment with a Process and Tools Using Norms and Example) The main objective of the NEPTUNE project is to develop both a method and tools (complementary to the existing software environments) based on the use of the UML notation. This method, gained from considerable experience in the industrial environment, will apply to a variety of different fields: software development, business processes and knowledge management. The newly developed tools will enable to be statically check UML models for their coherence. They will also enable generation of professional documentation resulting from the transformation of models. This will be compliant with the context of the UML notation and will take into account user's requirements. The method and tools developed in this way will facilitate the application of the UML standard as well as promoting its use in a large number of varied fields. http://neptune.irit.fr/

220
Noeth, W., Handbuch der Semiotik, 2nd ed., renewed and extended, Stuttgart - Weimar: J.B.Metzler Publisher

221
, Nöth, W. (Ed.), The Origins of Semiosis. Sign Evolution in Nature and Culture, Berlin - New York: Mouton de Gruyter, 1994

222
Norström, Chr.; Wall, A.; Yi, W. Timed automata as task models for event-driven systems, IEEE 1999

223
OKSIMO Projekt Open source software project for general simulations: http://www.oksimo.org

224
OMG MDA Guide Version 1.0.1 Document Number: omg/2003-06-01 Date: 12th June 2003 http://www.omg.org/docs

225
OpenEmbedded := OpenEmbeDD is a project of the ANR (Agence National de la Recherche). Its goal is to build an open-source plateform for Model Driven Engineering of Real Time and embedded systems. http://openembedd.inria.fr/home_html-en

226
Peirce, C. S., Collected Papers of Charles Sanders Peirce. Vols. 1-8, ed. by Charles Hartshorne; Pauls Weiss, Vols.7-8. ed. by Arthur W.Burks. Cambridge (MA): Harvard University Press. Citation with (CP, n.m) (n := Volume, m := Paragraph), 1931-58

227
Perrin, D. Finite Automata, in: Van Leeuwen, J. (Ed.), Handbook of Theoretical Computer Science. Formal Models and Semantics. Vol.B, Amsterdam: Elsevier & Ca,bridge (MA): The MIT Press, 1990; Pp.1-57

228
Petri Nets - Homepage: The purpose of the Petri Nets World is to provide a variety of online services for the international Petri Nets community. The services constitute, among other things, information on the International Conferences on Application and Theory of Petri Nets, mailing lists, bibliographies, tool databases, newsletters, and addresses. http://www.informatik.uni-hamburg.de/TGI/PetriNets/

229
Pnueli, A.The temporal logic of programs, In. Proc. 18th. IEEE Symp. Foundations of computer Science (FOCS'77), Providence, RI, USA, Oct.-Nov. 1977, Pp.46-57, 1977

230
Pnueli, A.The temporal semantics of concurrent programs, In.theoretical computer Science, 1381):45 - 60, 1981

231
Popovic, M.; Kovacevic, V.; Velikic, I.; A formal software verification concept based on automated theorem proving and reverse engineering, in: Engineering of Computer-Based Systems, 2002. Proceedings. Ninth Annual IEEE International Conference and Workshop on the, 8-11 April 2002 Page(s):59 - 66

232
Potthoff, K.; Einführung in die Modelltheorie und ihre Anwendungen, Darmstadt: Wiss.Buchgesellschaft, 1981

233
Presburger, M. (1929). Ueber die Vollstaendigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt". in: Comptes Rendus du Ier congresse des Mathematiciens des Pays Slaves. Warszawa: 92-101.

234
Prior, A. N., Time and Modality, Oxford: Clarendon Press, 1957

235
Prior, A. N., Past, Present and Future, Oxford: Clarendon Press, 1967

236
Prior, A. N., Papers on Time and Tense, Oxford: Clarendon Press, 1969

237
Pucdella, R.; The finite and the infinite in temporal logic, SIGACT News , Volume 36 Issue 1, Pages: 86 - 99, 2005, ISSN:0163-5700

238
Quielle, J.P.; Sifakis, J. Specification and verification of concurrent systems in CESAR, In: Proceedings of the 5th Intern.Symp. on Programming, 1981, Pp.337-350

239
Quine, W.v. (1964). Methods of Logic.(rev.ed.). New York et al: Holt, Rinehart and Wilson.

240
Rabin, M. O.; Scott, D. Finite Automata and their Decision Problems,in: IBM Journal of Research and Development, 3:2 (1959) pp.115-125

241
Reddy, C. R., and D. W. Loveland (1978). "Presburger Arithmetic with Bounded Quantifier Alternation." ACM Symposium on Theory of Computing: 320-325.

242
Reutenauer, C. Aspects mathématiques des réseaux de petri, Collection études et recherches en informatique, Paris: Masson, 1989

243
Robertson, S. & Robertson, J. (2006). Mastering the Requirements Process. (2nd ed.) Boston (Massachusetts): Addison-Wesley Professional

244
Robinson, A.; Voronkov, A. (eds.) (2001). Handbook of Automated Reasoning Volume I & II. Elsevier and MIT Press.

245
Rosser, John Barkley . (1936) "Extensions of some theorems of Gï¿12el and Church". In: Journal of Symbolic Logic 1: 87-91

246
Rozenberg, R., & Salomaa, A. (Eds.). (1997). Handbook of Formal Languages. Vol. 1-3. Berlin - Heidelberg - New York et al: Springer

247
Rupp, Chr. (2006). Requirements-Engineering und -Management. (4th ed.). Mnchen: Hanser Fachbuchverlag

248
Schienmann, B. (2001). Anforderungsmanagement: Prozesse - Techniken - Werkzeuge. Mnchen: Addison-Wesley

249
Schilpp, P. A. (Ed.). (1963). The Philosophy of Rudolf Carnap. London: Cambridge University.

250
Schneider, K. Verification of Reactive Systems. Formal Methods and Algorithms, Berlin-Heidelberg: Springer-Verlag, 2004

251
Schröter, K.; Was ist eine mathematische theorie?, in: Jahresbericht der deutschen Mathematikervereinigung (DMV), vol.53, pp.69-82, 1943 (Repr. in Berka, K.; Kreiser, L.; Logiktexte. Kommentierte Auswahl zur Geschichte der modernen Logik., 2nd. corr. ed., Berlin: Akademieverlag, 1973)

252
Shannon, C. E.; McCarthy,J., (Eds.) Automata Studies, (AM-34) Annals of Mathematics Studies), Princeton: Princeton University Press, 1956, (ISBN-10: 0691079161, ISBN-13: 978-0691079165)

253
Shaw, M.; DeLine, R.; Klein, D.V.; Ross, T.L.; Young, D.M.; Zelesnik, G. (1995). Abstractions for software architecture and tools to support them. Software Engineering, IEEE Transactions on, Volume 21, Issue 4, Date: Apr 1995, Pages: 314 - 335

254
Shoenfield, J.R.(1967). Mathematical Logic. Reading (MA) et al: Addison-Wesley Publ.Comp.

255
Shoham, Sh.; Grumberg, O.; A game-based framework for CTL counterexamples and 3-valued abstraction-refinement, In: ACM Transactions on Computational Logic (TOCL), Volume 9 , Issue 1 (December 2007), Article No. 1 , 2007, ISSN:1529-3785

256
Siekmann, J.H.; Wrightson, G., (Eds.) Automation of Reasoning 1: Classical Papers on Computational Logic, 1957-1966, Berlin: Springer, 1983,(ISBN-10: 0387120432, ISBN-13: 978-0387120430)

257
Siekmann, J.H.; Wrightson, G., (Eds.) Automation of Reasoning 2: Classical Papers on Computational Logic 1967-1970, Berlin: Springer, 1983, (ISBN-10: 3540120440, ISBN-13: 978-3540120445)

258
Smullyan,Raymond . (1991). Gï¿12el's Incompleteness Theorems. Oxford Univ. Press.

259
Sneed, J. D. (1979). The Logical Structure of Mathematical Physics (2nd.rev.ed.) Dordrecht - Boston - London: D.Reidel Publishin Company.

260
Solovay, R., (1989). "Injecting Inconsistencies into Models of PA". Annals of Pure and Applied Logic 44(1-2): 101?132.

261
Some, S.; Dssouli, R.; Vaucher, J. From scenarios to timed automata: building specifications from users requirements, In: Software Engineering Conference, 1995. Proceedings., 1995 Asia Pacific, Date: 6-9 Dec 1995, Pages: 48 - 57

262
Suppe, F. (Ed.). (1979). The Structure of Scientific Theories (2nd. ed.) Urbana: University of Illinois Press.

263
OMG-SysML, OMG Systems Modeling Language (OMG SysML$ ^{TM}$), V1.0, OMG Document Number: formal/2007-09-01, Standard document URL: http://www.omg.org/spec/SysML/1.0/PDF

264
Tarski, A.; Der Wahrheitsbegriff in den formalisierten Sprachen, In: Studia Philosophica 1 (1936), S. 261-404.

265
Tarski, A.; Einführung in die Mathematische Logik und in die Methodologie der Mathematik. Wien: Springer, 1937

266
Tarski, A.; The Semantic Conception of Truth and the Foundations of Semantics, In: Philosophy and Phenomenological Research IV, 3 (1944), S. 341-375. (Deutsche Übs. in: Gunnar Skirbekk, hrsg.: Wahrheitstheorien. Eine Auswahl aus den Diskussionen über Wahrheit im 20.Jahrhundert. Frankfurt am Main 1977, S. 140-188.)

267
Tarski, A.; Mostowski, A.; Robinson, R.M.; ): Undecidable theories, Amsterdam: North-Holland Publ., 1953. (= Studies in logic and the foundations of mathematics.)

268
Tarski, A.; Introduction to logic and to the methodology of deductive sciences, New York : Oxford University Press, 1965

269
Tarski, A.; Einführung in die mathematische Logik. Auf Grund d. engl. u. französ. Ausg. u. der Ergänzungen d. Verf. übs. v. Erhard Scheibe. 2., neubearb. Aufl. Göttingen: Vandenhoek & Ruprecht, 1966. (= Moderne Mathematik in elementarer Darstellung. 5.) 5. Aufl. (1977) mit Anhang "Wahrheit und Beweis" ISBN 3-525-40540-5.

270
Tarski, A.; Collected Papers, Ed. by Steven R. Givant u.a., 4 vols. , Basel/Boston u.a.: Birkhäuser, 1986.

271
Tasiran, S. et al. Verifying Abstractions of Timed Systems, research paper 1996

272
Thomas, W. Automata on Infinite Objects, in: Van Leeuwen, J. (Ed.), Handbook of Theoretical Computer Science. Formal Models and Semantics. Vol.B, Amsterdam: Elsevier & Cambridge (MA): The MIT Press, 1990; Pp.133-191

273
Thomas, W. Languages, Automata, and Logic, in: Rozenberg, G.; Salomaa, A. , handbook of Formal Languages. Vol.3. Beyond Words, Berlin: Springer, 1997; Pp.389-455

274
Turing, A. M. On Computable Numbers with an Application to the Entscheidungsproblem. In: Proc. London Math. Soc., Ser.2, vol.42(1936), pp.230-265; received May 25, 1936; Appendix added August 28; read November 12, 1936; corr. Ibid. vol.43(1937), pp.544-546. Turing's paper appeared in Part 2 of vol.42 which was issued in December 1936 (Reprint in M.DAVIS 1965, pp.116-151; corr. ibid. pp.151-154).

275
Turing, A. M.Intelligence Service. Schriften, ed.by. Dotzler, B.; Kittler, F., Berlin: Brinkmann & Bose, 1987

276
UPPAAL is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.). The tool is developed in collaboration between the Department of Information Technology at Uppsala University, Sweden and the Department of Computer Science at Aalborg University in Denmark. http://www.uppaal.com/

277
Viganò, F.; Colombetti, M.; Symbolic model checking of institutions, In: ICEC '07: Proceedings of the ninth international conference on Electronic commerce, Pages: 35 - 44, 2007, ISBN:978-1-59593-700-1 2007

278
V-Modell XT Gesamt 1.3, englisch, Format PDF, URL: http://v-modell.iabg.de/dmdocuments/V-Modell-XT-Gesamt-Englisch-V1.3.pdf, last change: 09.02.2009 10:04 , IABG Industrieanlagen-Betriebsgesellschaft mbH, Einsteinstraße 20, 85521 Ottobrunn

279
VASY := 'Validation of Systems': VASY is a research team of INRIA working in the area of formal methods applied to safety-critical systems. The research activities of VASY encompass formal specification languages and associated methodologies, compiling and rapid prototyping techniques, simulation, validation, verification, and testing. VASY develops advanced software tools, which are used in numerous case-studies, and is involved in several technology transfer projects with industrial partners. http://www.inrialpes.fr/vasy/

280
Van Heijenoort,Jean . (1963). "Goedel's Theorem," in Paul Edwards, ed., Encyclopedia of Philosophy, Vol. 3. Macmillan: 348-57

281
Wagner, F.; Schmuki, R.; Wagner, Th.; Wolstenholme, P. Modeling Software with Finite Machines. A Practical Approach, Boca Raton - New York: Auerbach Publications, 2006

282
F.Wang; G-H. Huang; F. Yu TCTL Inevitability Analysis of Dense-Time Systems: From Theory to Engineering, In: IEEE Transactions in SWE, July 2006 (Vol. 32, No. 7), pp. 510-526

283
Wang,Hao. (1997). A Logical Journey: From Goedel to Philosophy. MIT Press

284
Wendt, S. Die Modelle von Moore und Mealy - Klaerung einer begrifflichen Konfusion, Kaiserslautern. Universitaet, MS 1998

285
Weilkiens, T., Systems Engineering mit SysML/UML, Heidelberg: dpunkt.verlag, 2006

286
Wiegers, K.E. (2003). Software Requirements. (2nd.ed). Redmond: Microsoft Press

287
Wikipedia.org (2006). First informations about Automated Theorem Prooving:http://en.wikipedia.org/wiki/Automated_theorem_proving

288
Wikipedia.org (2006). First informations about Computational Tree Logic (CTL):http://en.wikipedia.org/wiki/Computational_tree_logic

289
Wikipedia.org (2006). First informations about Formal Logic: http://en.wikipedia.org/wiki/Logic

290
Wikipedia.org (2006). First informations about Formal Methods:http://en.wikipedia.org/wiki/Formal_methods

291
Wikipedia.org (2006). First informations about Model Checking:http://en.wikipedia.org/wiki/Model_checking

292
Wikipedia.org (2006). First informations about Verification: http://en.wikipedia.org/wiki/Formal_verification

293
Wikipedia.org (2006). First informations about Symbol Grounding: http://en.wikipedia.org/wiki/Symbol_grounding

294
Willard, D. (2001). "Self Verifying Axiom Systems, the Incompleteness Theorem and the Tangibility Reflection Princible". Journal of Symbolic Logic 66:536?596.

295
Willard, D., (2002). "How to Extend the Semantic Tableaux and Cut-Free Versions of the Second Incompleteness Theorem to Robinson's Arithmetic Q" . Journal of Symbolic Logic 67:465-496.

296
Woodcock, Jim: First Steps in the Verified Software Grand Challenge. IEEE Computer, IEEE Computer Society, October 2006, p. 57

297
Wong-Toi, H.; Hoffmann, G. The Control of Dense Real-Time Event Systems, In: Proceedings of the 30th IEEE Conference on Decision and Control, Brighton - England, 1527 - 1525, 1991

298
Wos, Larry, Overbeek, Ross; Lusk, Ewing; Boyle, Jim (1992). Automated Reasoning: Introduction and Applications, 2nd edition, McGraw-Hill.

299
Yamane, S. Hierarchical design method for real-time distributed systems, In: Real-Time Computing Systems and Applications, 1998. Proceedings. Fifth International Conference on, Date: 27-29 Oct 1998, Pages: 189 - 192

300
YU,S. Regular Languages, in: ROZENBERG.G.; SALOMAA, A. (Eds.) Handbook of Formal Languages, Vol. 1-3, Springer Verlag, Heidelberg - Berlin et al., 1997. Vol.1, pp41-110

301
Z-Notation Tools at: http://czt.sourceforge.net/

302
Zeta-System (an open environment for the development of specification documents based on Z.): http://uebb.cs.tu-berlin.de/zeta/



Gerd Doeben-Henisch 2010-03-03