当前位置：文档之家 › Short Description Automata with substitutions, Fusion and Bindings, Models for Open π-calc

Short Description Automata with substitutions, Fusion and Bindings, Models for Open π-calc

  • 格式：pdf
  • 大小：68.84 KB
  • 文档页数：11

DELIVERABLESUMMARYSHEETProjectNumber:IST-2001-33100ProjectAcronym:PROFUNDISTitle:ProofsofFunctionalityforMobileDistributedSystems

DeliverableNumber:3Duedate:Projectmonth36Deliverydate:March14,2005

ShortDescription:Automatawithsubstitutions,FusionandBindings,ModelsforOpenπ-calculusanddistinctions,ModelsofSpatialLogics.

SymbolicVerificationofSecurityProtocols.VerificationServicesandCaseStudies.

Partnersowning:DipartimentodiInformaticaUniv.Pisa,ItalyPartnerscontributed:Uppsala,FFCTLisbon,INRIA,PisaMadeavailableto:

1Contents1Overview32ScientificContributions32.0.1Task1.1:AutomatawithOperationsandSubstitutions.32.0.2Task1.2:ProofTechniques.................52.0.3Task1.3:PrototypeandCaseStudies...........52.1UpdateSecondYearReport.....................6

3Appendix:WP1ScientificContributions94Appendix:WP1UpdatedVersions10

21OverviewTheoverallgoalofthisWorkPackageistodevelopacomprehensiveautomata-likemodelthatsupportseffectivetechniquestospecifyandverifypropertiesofnetworkapplications.TheactivitiesonTask1.1.(Automatawithoperationsandsubstitutions)wereexpectedtobecompletedbytheendofthesecondyear.However,wemodifiedourinitialplansandwecontinuedthemalsointhethirdyear.Hence,foryear3thespecificobjectiveforTask1.1includeautomatawithsubstitutions,higherorderabstractsyntaxandfunctorialsemantics,and(bialgebraicandfunctorial)modelsfordistinctions(openπ-calculus,fusion)andmodelsforspatiallogics.ForTask1.2wecontinuedthedevelopmentofprooftechniques(typicallyofsecurityprotocols)basedonsymbolicexecution.Task1.3.wasconcernedwithextendingtheProfundistoolkitinfrustructure(thePweb).Moreover,wetoassessourverificationinfrastructurewefocussedonsomecasestudies.ThisdeliverableincludesthescientificcontributionsofthethirdyearforWP1.Thedeliverableconsistsofashortpresentationofthecontributionsandofseveralappendiceswiththecontributedpapers.

2ScientificContributionsTheresearchactivitiesofalltaskshaveadvancedwell,providingsomeresultsintermsofbothpublicationsandexperimentation.Hereafter,wewillbrieflysummarizetheresultsoftheresearchactivitiesofthethirdyearforeachofthethreetasks.

2.0.1Task1.1:AutomatawithOperationsandSubstitutionsAutomatawithsubstitutionsandBialgebraicmodelsTheformulationofHD-automataasthebasicmodelfornamepassingprocesscalculihasbeenfurtherdeveloped.Duringthethirdyear,wedeveloped[13]ageneralframe-worktodescribethesymbolicsemanticsofnominalcalculi,whereinputsarerepresentedasvariableswhichareinstantiatedonlywhenneededasithappensinlogicprogramming.TheapproachwefollowreliesonthenotionsofreactivesystemandofobservableborrowedcontextsintroducedbyLeiferandMilnerandfurtherdevelopedbySassone,LackandSobocinskiusingG-categoriesandadhesivecategories.Thereductionsemanticsofreactivesystemsisextendedinordertointroduceasborrowedcontextsboththevariableinstantiationsneededinthetransitionsandtheordinaryπ-calculusactions.Theproposedmodelcannaturallydescribeinteractionswithbindingmechanismscanbeconvenientlyappliedtohandlewebservicediscoveryandinvocations.Bialgebraicmodelsofprocesscalculienjoythepropertythatbisimilarityisacongruence.Indeed,theuniquemorphismtothefinalbialgebrainducesabisimilarityrelationwhichcoincideswithobservationalequivalenceandwhichisacongruencewithrespecttotheoperations.However,theapplicationofthebialgebraicapproachtopro-cesscalculiwithstructuralaxioms(e.g.namepassingprocesscalculi)ismore

3problematic,becauseoftheinteractionbetweenaxiomsandinferencerules.In[16],weintroduceageneralapproachtoliftcalculiwithstructuralaxiomstobialgebras.Inorderfortheliftingtohold,twoconditionsarerequired:thetran-sitionrulesofthecalculusareintyftformatandtheaxiomsbisimulatewithrespecttothelts.In[17]weprovideacompositionalcoalgebraicsemanticsoftheFusioncalculus.Inourmodel,theuniquemorphismtothefinalbialgebrainducesabisimilarityrelationwhichcoincideswithhyperequivalenceandwhichisacongruencewithrespecttotheoperations.

FunctorialSemanticsforNominalCalculiWehaveheretwolinesofre-search,allaimingatthedevelopmentofabstractmodelsfornomicalcalculi.ThefirstlineofresearchdevelopedatUppsalaconcernsthedevelopmentoffunctorialmodelsfornames.In[15]thetechniquesofhigherorderabstractsyntaxandfunctorialoperationalsemanticshavebeenextendedtogiveacleanpresentationofopenbisimularity.Akeyresultshowsthatopenbisimulationrequiresustomovefromtheusualsemanticdomainofpresheavesoversubcate-goriesofSettopresheavesoversubcategoriesofRel.In[18]acategorytheoreticmodelwhereboth“variables”and“names”,usuallyviewedasseparatenotions,havebeeninvestigated.Theproposalconsidersfunctorsoverthecategoryofirreflexive,symmetricfiniterelations.Themodelspreviouslyproposedforthenotionsof“variables”and“names”embedfaithfullyinthenewone,andini-tialalgebra/finalcoalgebraconstructionscanbetransferredfromtheformerstothelatter.ThesecondlineofresearchdevelopedinPisa[14]aimsatpro-vidingageneralframeworktorelatethedifferentabstractmodelsofnominalcalculi,namely(pre)sheafcategories,nominalsets,permutationalgebrasandnamedsets.Therelationshipsamongthesemodelshavebeenstudiedandtheproposedframeworwallowsonetotransfertechniquesandconstructionsfromonemodeltotheother.

合集下载

形式语言与自动机

形式语言与自动机


0
1
1
0
q1
q2
q3
0,1
8
有穷自动机的形式定义
定义 1.1 有穷自动机是一个 5 元组 ( Q, , , q0, F )，其中 (1) Q 是一个有穷集合，称为状态集。 (2) 是一个有穷集合，称为字母表。 (3) : QQ是转移函数。 (4) q0Q 是起始状态。 (5) FQ 是接受状态集。 介绍写定义的方法：元组式，递归式… Let 式 : Let, It is said to be …. If …….
0 0 0
0
0
32
非确定性
例1.16 考虑图示的 NFA N 。运行这台机器，判断其是否识别 ε、a、baba、baa、b、bb、babba。
q1
a b q2 a, b a q3
为了识别A1∪A2和，机器M必须恰好在M1或M2接受的时候
接受他的输入串。M模拟M1和M2并且当这两个模拟中有一
个接受时，M接受。
22
正则运算
定理 1.12 正则语言类在并运算下封闭。
如果A1和A2是正则语言，则A1∪A2也是正则语言。
设 M1 识别 A1， M2 识别 A2。并设
M1=(Q1, , 1,q1, F1) 和 M2=(Q2, , 2, q2, F2) 构造识别A1∪A2 的 M=(Q, , , q0, F)
Q = Q1Q2 = {(r1, r2) | r1Q1 且 r2Q2} ((r1, r2), a ) = (1(r1,a), 2(r2,a) ) q0 = (q1, q2) F = {(r1, r2) | r1F1 或 r2F2}
23
REVIEW(2011-03-07)
确定有限自动机的形式化定义 ( Q, , , q0, F ) 机器识别语言 若 A 是机器 M 接受的全部字符串集，则称 A 是机器 M 的语 言，记作 L(M)=A，又称 M 识别 A 或 M 接受 A。 计算的形式化定义
scheme中文教程

scheme中文教程


C. HANSON
K. M. PITMAN
M. WAND
谨以此纪念 Robert Hieb
1998 年 2 月 20 日
摘要
本报告给出程序设计语言 Scheme 的定义性描述。 Scheme 是 Lisp 程序设计语言的方言，由 Guy Lewis Steele Jr. 和 Gerald Jay Sussman 发明，具有静态作用域和严格尾递归 的特点。它的设计目标是拥有异常清晰、简明的语义和较 少的表达式异构方式。包括命令式、函数式和消息传递式 风格在内的绝大多数程序设计模型都可以用 Scheme 方便 地表述。
whitespace 6 with-input-from-file 32 with-output-to-file 32 write 33; 13 write-char 33
#x 19; 35
zero? 20
Index 47
算法语言 Scheme 修订5报告
王咏刚 试译 v 0.9.5
RICHARD KELSEY, WILLIAM CLINGER, AND JONATHAN REES (编者)
第 7 章用扩展 BNF 给出了 Scheme 语言的形式语法，并为 其定义了形式指称语义。形式语法和语义后面有一个使用 Scheme 语言的示例。
本报告的最后是参考文献列表和依字母顺序排列的索引。
目录
概述 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1 Scheme 概论 . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
#t 23 tail call 尾调用 7 tan 21 token 记号 34 top level environment 最高层环境 16; 6 transcript-off 34 transcript-on 34 true 7; 10, 23 truncate 21 type 类型 7
Contributions

Contributions


A Proof Environment for Specifications
March th,

/ in a Nutshell
e Object Constraint Language ()
Textual extension of the Allows for annotating diagrams In the context of class–diagrams:
invariants preconditions postconditions
Practice:
A machine checked semantics for .
Achim D. Brucker ( Zurich)
A Proof Environment for Specifications
March th,

/ in a Nutshell
context Account inv: 0 <= id
Account balance:Integer id:Integer 1..* getId():Integer accounts getBalance():Integer deposit(a:Integer):Boolean withdraw(a:Integer):Boolean
Achim D. Brucker ( Zurich)
A Proof Environment for Specifications
March th,

/ in a Nutshell
The Object Constraint Language ()
e Object Constraint Language ()
Outline
使用延时演算的时间化rsl的指称语义

使用延时演算的时间化rsl的指称语义

摘要《ＲＡｌＳＥ描述语言（ＲＳＬ）是用于形式化地描述、设计和开发软件的最通用和最全面的语言之一．它已经被扩展到时间化ＲＳＬ来描述与时间有关的操作．但是，它不具有在抽象层次上描述实时需求的特征．延时演算（ＤｕｒａｔｉｏｎＣａｈ’ｌｌｈｌｓ）是一种实时区间逻辑．它已经被广泛用于实时系统设计的描述和验证．但是，它不支持数据结构、算法和模块化设计．混成系统是包含离散部件和连续部件的实时系统．扩展的延时演算（ＥｘｔｅｎｄｅｄＤｕｒａｔｉｏｎＣａｌｃｕｌｕｓ）将延时演算扩展到了混成系统．）本文的目的是，通过用扩展的延时演算为命令式的时间化ＲＳＬ表达式定义指称语义，结合时间化ＲｓＬ和延时演算，以用于混成系统的形式化描述、验证、设计和开发．：在时间化ＲＳＬ中，外部选择是指由表达式在不同的分支中提供不同的通讯选择，由外部环境来决定进行哪一个通讯，以使表达式执行相应的分支．超时选择是指其它分支只能在一定时间之内被选择，否则表达式将执行超时分支．本文通过结合外部选择和超时选择，扩展了时间化ＲＳＬ，大大简化了许多代数定律。

离散状态变量的意义是离散的时间函数．在扩展的延时演算中，离散状态变量只能是布尔类型，项只有通过关系操作符的连接才能成为公式．本文改进了扩展的延时演算，使得离散状态变量可以是任意类型，并将任何布尔类型的项作为公式，增加了灵活性和表达性．为了形式化描述串行构造、循环及程序变量的稳定状态，本文在扩展的延时演算模型中加入一些高级特征，并探究它们的代数性质．这些性质对于实时程序的形式化和实时性质的验证起着关键作用．时间化ＲＳＬ的基本元素是变量和用于通信的通道，并且每一个命令式的时间化ＲＳＬ表达式都有一个返回值．时间化ＲＳＬ表达式的行为可以划分为三种类型：发散、等待和终止．我们基于对通道、变量和返回值的观察，使用带有高级特征的扩展的延时演算公式，定义了时间化ＲＳＬ的指称语义，它能够用单一的公式描述所有类型的表达式行为．从我们所定义的指称语义。