摘要：描述:时间排序规范语言(LOTOS),是以带有来自相关代数学CSP和电路计算(CIRCAI.)附加特征的CCS为基础的。它通过结合基于抽象数据型语言ACT ONE从而克服了CCS在处理数据结构和值表示式方面的羽点，然而在描述抽象数据类型时可使用LOTOS的过程
C.2.4.5 时间排序规范语言(LOTOS)
目的:LOTOS是用于描述和推理并行通信过程系统行为的一种方法。
描述:时间排序规范语言(LOTOS),是以带有来自相关代数学CSP和电路计算(CIRCAI.)附加特征的CCS为基础的。它通过结合基于抽象数据型语言ACT ONE从而克服了CCS在处理数据结构和值表示式方面的羽点，然而在描述抽象数据类型时可使用LOTOS的过程描述成分并结合其他形式化方法。
参考文献:
Model Checking for Software Architectures. R.Matcescu.In Software Architecture,Lecture Notes in Computer Science,Springer Berlin/ Heidelberg,2004.1SBN 978-3-540-22000-8
ISO 8807:1989.Information processing systems-Open Systems Interconnection-LOTOS-A fornal description technique based on the temporal ordering of observational behaviour
C.2.4.6 OBJ
目的:为了在实现之前利用用户反馈信息和系统确认信息提供一个精确的系统规范。
描述:OB]是一种代数规范语言，用户将要求规定为代数方程的形式，通过影响抽象数据类型(ADT)的运算,规定系统行为成结构特征，一个ADT就像一个ADA包一样,只不过运算符的工作情况可见而实现细节是“隐藏"的。
一种OBJ规范和其后的逐步实现适合于同其他形式化方法一样的形式证明技术。此外,因为OBJ规范的结构特征可用机器执行,因此从规范本身可直接实现系统确认，执行过程实质上是通过持续的方程置换(重写)直到获得规定的输出值为止来评价一个功能，这种可执行性允许设想系统的最终用户在系统规范阶段就能够直观认识最终系统,而不需精选基础的形式规范技术。
正如其他所有的ADT技术的情况一样,OBJ只适用于顺序系统或者并行系统的顺序部分。OBJ已被用于各种规模的工业应用的规范。
参考文献:
Software Engineering with OBJ: Algebraie Specification in Action. J. Goguen, G. Malcolm, Springer, 2000,1SBN 0792377575.9780792377573
C.2.4.7 时序逻辑
目的:安全性和适行要求的直接表达式,及这些器性在其后的开发步骤中得以保持的形式化证明。
描述:标准的一阶谓词逻辑不包含时间概念.通过增加情态算符(例如"此后"(henceforth)和"最终”(eventally)),时序逻辑可扩展一阶逻辑，这些算符可用来限定有关系统的一些声明。例如,安全属性可能需要包含"此后”,而要求的系统的其他状态可能需要借助某些另外的起始状态达到"最终"。使用状态(行为)序列来解释时序公式，“状态”由何组成取决于选择的描述等级，它可以指整个系统,一个系统部件或者计算机程序。
在时序逻辑中并不直接处理销化的时间间隔相约束，必须通过建立附加的时间状态把绝对定时处理成状态描述的一部分。
参考文献:
Mathermatical Logic for Comoputer Science, M. Ben-Ari, Springer, 2001,ISBN1852333197.9781852333195
C.2.4.8 VDM,VDM++一维也纳(Vienna)开发方法
目的：顺序(VDM)和并行实时(VD)M+十)程序的系统化规范和实现。
描述：VDM是基于数学的一种规范技术,通过允许依据规范证明其正确性来细化实现。
规范技术是以模型为基础的,该技术将系统状态建模为集合理论结构(基于结构描述的不变量(谓词)),以及通过将其先决和后置条件规定为系统状态来进行建模的状态的运算，为了保留系统不变量，可验证这些运算。
通过将系统状态具体化为目标语言的数据结构,并通过将运算细化为目标语言的程序,可完成规范的实现，具体化和细化步骤将引出证明它们的正确性的责任。设计者应决定是否要履行这些职责。
原则上讲,VDM用在规范阶段,但也可在产生源码的设计和实现阶段中使用。它仪适用于并行系统中顺序结构程序或者顺序过程。
面向对象的和并行实时扩充的VDM,即VDM++,是基于ISO语言VDM-SL和面向对象的语言 Smallualk的一种形式规范语言。
VDM++提供了一个很宽的结构范围,因而用户可在形式上用一种面向对象的格式来规定实时系统。在VDM++中,一个完整的形式规范由分类规范的一个汇集和任选的一个工作区组成。
VDM++的实时规定是:
——为了表示一个方法主体中的当前时刻和方法引用时刻,应提供时序表达式;
——给方法增加一个定时的后续表达式以便为正确实现规定执行时间的上(或下)限;
——已经引入时间连续变量。利用假设子句和效果子句,可以规定这些时间函数之间的关系(例如微分方程)。这个特征已证明对工作在一个时间连续环境中的系统要求的规范是很有用的。细化步骤可产生这些类型的系统的离散软件解。
参考文献:
ISO/IEC 13817-1:1996.Information technology-Programming languages, their environments and system software interfaces-Vienna Development Method-Specification Language-Part 1: Base language
Systematic Software Development using VDM.C.B.Jones.Prentice-Hall.2nd Edition,1990
Conformity Clause for VDM-SL,G.1.Parkin and B.A.Wichmann, Lecture Notes in Computer Sei- ence 670,FME’93 Industrial-Strength Formal Methods, First International Symposium of Formal Methods in Europe.Editors:J.C.P,Woodcock and P.G.Larsen.Springer Verlag,501-520
C.2.4.9 Z
目的:Z是用于顺序系统的一种规范语言表示方法,也是一种允许开发者从一个Z规范开始进行可执行的算法的设计技术,该算法允许对照规范验证它们的正确性。
Z主要用于规范阶段,但也已延伸至设计和实现。它最适合于开发面向数据的顺序系统。
描述：像 VDM一样,规范技术是以模型为基础的.该技术将系统状态建模为集合理论结构[基于结构描述的不变量(谓词)],以及通过将其先决和后置条件规定为系统状态来进行建模的状态的运算。为了保留系统不变量从而证实其一致性可证明这些运算,将把一个规范的形式部分分成一些模式，这些模式允许通过细化构建规范。
典型地，一个Z规范是形式Z和用自然语言的非形式化说明文本的混合物(形式化文本本身过于简要因而不易读，并且常常需要解释它的目的,而非形式化自然语言容易变得模糊和不准确)。
与VDM不同,Z是一种表达式而不是一个完整的方法,然而已开发出一种辅助方法(称为B),它可同Z一起使用。B方法依据的是逐步细化的原理。
参考文献:
Formal Specification using Z. 2nd Edition. D. Lightfoot, Palgrave Macmillan,2000.ISBN9780333763278
The B-Method.S.Schneider.Palgrave Macmillan,2001,1SBN 9780333792841
来源：细心教育