1、Xiaoju Dong(董笑菊)Joint course with Prof. Yuxi Fu(傅育熙)BASICS, Shanghai Jiao Tong Uhttp:/ Theory,问题1,公安机关正在调查一宗盗窃案，现获得事实如下： A或B盗窃了文物若A盗窃了文物，则作案时间不可能在午夜前若B证词正确，则在午夜前屋里灯光未灭若B证词不正确，则作案时间发生在午夜前午夜时屋里灯光灭了试问谁是盗窃犯？,2018年9月25日星期二,BASICS,2,问题1,公安机关正在调查一宗盗窃案，现获得事实如下： A或B盗窃了文物若A盗窃了文物，则作案时间不可能在午夜前若B证词正确，则在午夜前屋里灯光未灭
2、若B证词不正确，则作案时间发生在午夜前午夜时屋里灯光灭了试问谁是盗窃犯？,2018年9月25日星期二,BASICS,3,命题逻辑,问题2,电灯开关两个开关A、B同时控制一盏灯C,只要有一个开关处于开启状态灯就会亮只有两个开关之一处于开启状态灯才亮请具体列出灯C在开关A和B处于什么情况下会亮,问题2,电灯开关两个开关A、B同时控制一盏灯C,只要有一个开关处于开启状态灯就会亮只有两个开关之一处于开启状态灯才亮请具体列出灯C在开关A和B处于什么情况下会亮,数字逻辑,Formal Methods,In computer science, specifically software engineerin
3、g and hardware engineering, formal methods are a particular kind of mathematically based techniques for the specification, development and verification of software and hardware systemsThe use of formal methods for software and hardware design is motivated by the expectation that, as in other enginee
4、ring disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.,2018年9月25日星期二,BASICS,6,Formal Methods,Formal methods are best described as the application of a fairly broad variety of theoretical computer science fundamentals, in particula
5、r logic calculi, formal languages, automata theory, discrete event dynamic system and program semantics, but also type systems and algebraic data types to problems in software and hardware specification and verification,2018年9月25日星期二,BASICS,7,Xiaoju Dong(董笑菊)Joint course with Prof. Yuxi Fu(傅育熙)BASIC
6、S, Shanghai Jiao Tong Uhttp:/ Theory,9,Concurrency,In computer science, concurrency is a property of systems several computations are executing simultaneouslyand potentially interacting with each other,10,Concurrency,Computation any type of calculationuse of computer technology in Information proces
7、sing (e.g. query in a database)(electronic)computers, quantum computers, DNA computers, molecular computers, etc.a process following a well-defined model expressed in an algorithm, protocol, etc.,11,Concurrency,Interaction (or communication)Hand-shaking (synchronization)Value-passingName-passingProc
8、ess-passing,12,Concurrency,An example sorting,sequential,concurrent,concurrent (with interaction),13,Concurrency,An example sortingMore examples ?,14,Concurrency,An example sortingMore examples ?reading & eating an applechatting & downloadingCS web servicecells in our body,15,Concurrency theory,An a
9、ctive field of research in theoretical computer scienceFormalisms for modeling and reasoning about concurrencyOne of the first proposals: Carl Adam Petri, Petri Nets, in the early 1960s,Complex concurrent systems,Shared resources(1) x := 1 Sequential: determinedConcurrency: non-determined,(2) x := 0
10、 x := x+1,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,17,Content,Process calculiCalculus of Communicating Systems (CCS)Name Passing Calculus (Pi calculus)Petri nets,References,CCSCommunication and Concurrency.Robin Milner. Prentice Hall, 1989. Pi calculusCommunicating and Mobile Systems: The -calculus. Robin
11、Milner. Cambridge University Press, 1999. The -calculus: A Theory of Mobile Processes. Davide Sangiorgi. Cambridge University Press, 2001. Petri netsPetri nets an introduction ,Wolfgang Reisig, Springer-Verlag, 1982,Review,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,20,Sequential Computation,The Concept of Co
12、mputationSequential Computationa linearly ordered sequence of atomic actions,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,21,Some Models,Theory of Sequential ComputationTuring machine (Turing)Computation as mechanical operation-Calculus (Church)Computation as -reductionRecursion theory (Kleene etc.) Computatio
13、n as function compositionComputation denotes function,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,22,Turing Machine,A Turing machine is a theoretical device that manipulates symbols on a strip of tape according to a table of rulestape head transition function (a table of instructions, an action table)state re
14、gisterReferenceElements of the theory of computation, Harry LewisIntroduction to Theory of Computation, Michael Sipser,Turing Machine,2018年9月25日星期二,BASICS,23,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,24,-Calculus,Computation as Term RewritingTermt := x variable tt application x.t abstractionReduction(x.t)s
15、ts/xExamples: (x.xx) (x.xx) (x.xx) (x.xx)u(x.t)s) u(ts/x) (x.f(xx) (x.f(xx) f(x.f(xx) (x.f(xx),Fixed Point Theorem,For all lambda expressions F there exists X such that FX=X.Proof. Suppose W x.F(xx) and XWW. X WW (x.F(xx)W = F(WW) FX.,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,26,Recursive Function,Computabl
16、e Functions as Recursive FunctionsBasic IdeaSome initial functionsSome rules to compose new functionsCompositionRecursionMinimalization,Recursive Function,The Zero functionf(x) = 0The Successor functionf(x) = x+1The Projection functionf(x1, , xn, i) = xiSubstitution/compositionf(y1, , yn)=f(g(x1), ,
17、 g(xn), where yi=g(xi),2018年9月25日星期二,BASICS,27,Recursive Function,Recursionh(x, 0) = f(x); h(x, y+1) = g(x, y, h(x, y) e.g. x+y: x+0=x; x+(y+1)=(x+y)+1Minimization,2018年9月25日星期二,BASICS,28,Ackermann Function,2018年9月25日星期二,BASICS,29,The Ackermann function is not primitive recursive.It grows faster tha
18、n all the primitive recursive functions.,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,30,Church Turing Thesis,FactEquivalence in terms of expressive powerChurch Turing ThesisThe computable functions are precisely the recursive functionsLogical foundation of computationComputation as logical object,2018年9月25日星期
19、二,上海交通大学计算机系BASICS实验室,31,Concurrent System,All Systems are Concurrent SystemsConcurrency is an Intrinsic PropertyConcurrency is a Property Rather Than a Definition,EXAMPLES,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,33,Example I: Ether Net,Medium,Sender,Receiver,Is the Capacity of Medium Unbounded?Is the Ord
20、er of the Message Respected?,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,34,Example II: Vending Machine,Vending MachineThe slot can accept 1c coinThe buttons can be pressed for a cup of tea or coffeeTea or coffee can be collected from the trayInteraction between Machine and Buyer,2018年9月25日星期二,上海交通大学计算机系BASIC
21、S实验室,35,Transition,The State TransitionBlue is the initial stateGreen is the state after receiving 1cOne of the other two states is reached after the tea-button or the coffee-button is pressed,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,36,Nondeterminism,The Vending Machine Out of OrderHaving taking in 1c, th
22、e vending machine disable the tea-button or coffee-button nondeterministically,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,37,Equivalence,Are The Two Systems Equivalent?They are equivalent as automataAs concurrent systems they are not equivalent, because the ways buyers interact with them are differentObserva
23、tional Equivalence,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,38,Example III: Concurrent Program,Sequential ProgramsX:=2X:=1; X:=X+1Both Programs Assigns 2 to XTwo Programs are Equivalent,Concurrent ProgramsX:=2 | X:=2(X:=1; X:=X+1) | X:=2The Results are NondeterministicTwo Programs are not EquivalentInterle
24、aving semantics,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,39,Example IV: A Unit Transmitter,The transmitter receives a message through inIt sends out a message through outRepeat,C,in,out,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,40,Connecting Unit Transmitter,C,in,out,C,C,.,How does it behave?,n-times,2018年9月25日星期二
25、,上海交通大学计算机系BASICS实验室,41,Example V: Transmitter with Acknowledgment,The transmitter receives a message through inIt sends out a message through outIt receives acknowledgment through ackoutIt sends acknowledgment through ackinRepeat,D,in,out,ackout,ackin,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,42,Example V:
26、 Transmitter with Acknowledgment,D,in,out,ackout,ackin,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,43,Chaining Acknowledgment,D,in,out,D,D,.,ackout,ackin,n-copies,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,44,Chaining Acknowledgment,D,in,out,D,D,.,ackout,ackin,n-copies,How does it behave?,2018年9月25日星期二,上海交通大学计算机系BASIC
27、S实验室,45,Concurrent Computation,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,46,Models of Concurrent Computing,Petri Net (Petri;1962)Information flow in concurrent systemsProcess Algebra (Bergstra;1970s)Purely algebraic approachProcess Calculus (Milner, Hoare;1970)Operational approachSubject to studies of combi
28、ned approach,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,47,Concurrency Theory,Studies on Semantic Models forDistributed computingConcurrent ComputingMobile computing (mobile computation)Grid ComputingGlobal ComputingInternet ComputingCasts Light on Our Computing Practice,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,48,
29、Concurrency Kaleidoscope,Too Rich to be Understood at the MomentToo Rich to be Captured by one FormalismMany Complimentary Theories are Available,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,49,Process Calculus,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,50,Fundamental Questions,Some Fundamental Questions:What is a proc
30、ess?How to describe a process?What does a process do?When are two processes equivalent?No Definite Answers, Of Course!Research on the theory of process calculus proposes approximate answers,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,51,Analogy to -Calculus,-Terms ProcessesWhat are processes?Application Concu
31、rrent CompositionThe fundamental operation for process calculiReduction CommunicationCommunications are atomic actions,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,52,The Mottos of Process Calculus,Motto 1All computing objects are processes; There are no other computing objectsMotto 2All computing actions are
32、communications; There are no other kinds of actionsMotto 3A process lives to communicate,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,53,Syntactical Entities,Communications Happen through ChannelsTwo Classes of Syntactic ObjectsChannelsProcesses,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,54,Three Process Calculi,CCS Ca
33、lculus of Communicating SystemsMilner;1969CSP Communicating Sequential ProcessesHoare;1970-Calculus Milner,Parrow,Walker;1989,Robin Milner(1934-2010),1991 Turing AwardThree distinct and complete achievements:LCF, the mechanization of Scotts Logic of Computable Functions, probably the first theoretic
34、ally based yet practical tool for machine assisted proof constructionML, the first language to include polymorphic type inference together with a type-safe exception-handling mechanismCCS, a general theory of concurrency. In addition, he formulated and strongly advanced full abstraction, the study o
35、f the relationship between operational and denotational semantics,2018年9月25日星期二,BASICS,55,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,56,Books,Communication and ConcurrencyMilner, Prentice Hall, 1989Communicating Sequential ProcessesHoare, OUP, 1980Communicating and Mobile Systems: the -calculusMilner, CUP, 1
36、999The Pi-Calculus: a theory of mobile processesSangiorgi and Walker, CUP, 2001,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,57,Papers,A Calculus of Mobile ProcessesThe Pioneering PaperMilner, Parrow and WalkerInformation and Computation, 1992An Introduction to the - CalculusJ.Parrow. Chapter of Handbook of Pr
37、ocesses Algebra. Elsevier. 2001Elements of interactionR.Milner. Communication of ACM, (Jan):78-89, 1993,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,58,Websites,Website for Mobile Processhttp:/lampwww.epfl.ch/mobility/,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,59,Pure CCS,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,60,Content,S
38、yntaxSemanticsCounter,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,61,What is CCS about?,CCS, The Calculus of Communicating Systemsa formal language that models the operational behaviors of the communications of concurrent objects,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,62,How is CCS Defined?,The definition of CCS f
39、ollows the standard approach of defining a programming languageThe standard approach is widely used in computer science to define various calculi,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,63,Definition of Calculus,Defining Programming LanguagesSyntax Syntactical entityAlphabetBNF (Backus-Naur Form 巴科斯范式)Sem
40、anticsOperational behaviorLabeled Transition System, LTS,Operational Semantics,A way to give meaning to computation in a mathematically rigorous wayOther approaches to providing a formal semantics of computation include axiomatic semantics and denotational semanticsClassified into two categoriesstru
41、ctural operational semantics (small-step semantics)formally describe how the individual steps of a computation take place in a computer-based systemnatural semantics (big-step semantics) describe how the overall results of the executions are obtained,2018年9月25日星期二,BASICS,64,2018年9月25日星期二,上海交通大学计算机系B
42、ASICS实验室,65,Intuition about the Semantics,A = a.A, A = c.A; B = c.B, B = b.BExampleNa + Cl NaCl,def,def,def,def,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,66,Preliminary Notations,Action,ExternalInternal,Action,ExternalPotential to communicateInternal,Action,ExternalPotential to communicateInternalCommunicat
43、ion in a processCommunication between processes,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,70,Syntax of CCS,The abstract grammar is defined as follows:E := 0 nil process X process variable .E prefix E | E concurrent composition EL restriction Ef re-labeling E + E non-determinism A recursionWhere is either a
44、or a or , L N f: A A , a re-labeling function from A to ALet E be the set of process expressions and P be the set of processes,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,71,Intuitive Explanation,0The process that can never do anything in any environmentXProcess variable.EThe process that must first perform t
45、he action and then evolves as EE|EThe processes E and E may evlove independently or communicate through common channels,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,72,Intuitive Explanation,ELThe process that can do whatever E may do as long as the action are not restricted by LEfWhatever E can do, Ef can do w
46、ith action renamed by fE+EThe process that acts either as E or as EAThe recursive process that may never stop,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,73,What is an LTS?,E.G. automata,2018年9月25日星期二,上海交通大学计算机系BASICS实验室,74,An Example: The -Calculus,Termt := x variable tt application x.t abstractionReduction(x.t)s ts/xIf t t then st stIf t t then ts ts If t t then x.t x.t,
