-
- 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 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. -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), 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