全球研究计算机科学杂志》上
菜单石头:2229 - 371 x
石头:2229 - 371 x
蒙纳巴特拉1,阿米特·马利克2博士Meenu戴夫3
|
| 相关文章Pubmed,谷歌学者 |
访问更多的相关文章全球研究计算机科学杂志》上
当前信息系统的需求越来越将使用更高程度的形式主义在开发过程中。正式的方法由一组工具和技术的基于数学模型和形式逻辑用于指定并验证硬件和软件系统的需求和设计。本文详细分析正式的方法以及他们的目标和利益限制紧随其后。本研究工作的目的是帮助软件工程师确定正式的使用方法在软件开发的不同阶段,有特殊需求阶段的引用。
关键字 |
| 正式的方法,需求工程,正式规范、可行性分析等。 |
介绍 |
| 在今天的商业环境中,软件项目的主要衡量成功的程度是一个软件系统实现的目的,它的目的是。然而,竞争日益激烈的市场通常要求更高的质量,较短的周转周期,和便宜的软件。许多IT公司面临的困难按时发布产品的质量和批准的预算范围内。在开发过程中发现的错误数量强烈影响上述软件度量。如果前面问题是确定在程序开发,那么它有助于减少项目预算[1]。 |
| 当一个错误是在需求阶段引入的是发现在测试过程中,软件工程师必须解决错误的要求,检查所有的影响,通过设计和实现,最后重新测试产品。为了建立一个安全的软件产品,克服预算超支的问题(由于错误发生在需求规格),具有成本效益的方法要求解决的主要风险和提供有形证据的可信度。 |
| 正式的方法是解决上面提到的问题。正式的方法是一种特殊的数学技术用于规范,软件和硬件系统的开发和验证。表示用于正式的方法称为正式的规范语言。[2]。 |
| 正式的方法包括写正式的描述,这些描述和分析在某些情况下产生新的描述。他们可以应用在开发过程的不同阶段。他们甚至成为标准的主要组件。根据Rushby[3],在设计和施工中使用数学,以确保产品质量在建立工程学科中很常见,如桥或飞机,甚至计算机(硬件)建筑,其中一个表示物理数学和其他自然法则适用于模型问题,处理具体的系统在物理世界的行为。 |
| 本文描述了正式的方法在需求工程的各个方面。正式的规范语言,正式规范不同风格和类型的正式的第二节中描述的方法。在第三节,目标的正式方法解释而在第四节详细讨论了正式的方法的好处。在第五部分,提出了限制,第六节的问题。结论和未来的工作报告在第七节。 |
类型的正式的方法 |
| 正式的方法是基于数学的语言、技术和工具,可以应用于任何项目生命周期的一部分。通过提供抽象的特性和明确的描述机制,正式的方法促进发展的关键系统。表示用于正式的方法称为正式的规范语言。正式的规范语言是基于集合理论和一阶谓词演算。语言有一个正式的语义,可以用来表达规范清晰和明确的方式。正式的方法可以使用两种方法分类。首先,根据正式规范风格,其次,根据软件开发生命周期的视角[4]。 |
类型的正式规范风格 |
| 指定的正式规范样式如下: |
| 基于模型的语言: |
| 基于模型的语言编写一个规范的一种方法。指定系统的行为,基于模型的语言构建一个系统的数学模型。模型由一个潜在的状态(数据)和一组操作状态[5]。状态模型构造等的帮助下数学实体关系,集,序列和功能。操作系统通过定义指定它们如何影响系统的状态模型。谓词所描述的操作也给前后的条件。最广泛使用的符号为开发基于模型的开发方法(VDM),语言是维也纳Zed (Z)和B。 |
| 代数规范 |
| 代数规范是一种技术,用于指定使用方法来源于抽象代数系统行为。代数方法最初是专为抽象数据类型和接口的定义。发展中最广泛使用的符号代数规范语言是落叶松,美国手语和OBJ。 |
| 面向过程: |
| 面向过程的形式化规范语言基本上是用来描述并发系统通过构建一个特定的隐式模型。在这些流程是用表情和语言的帮助下建立了基本的表达式。基本表达式描述简单的流程以及操作,结合过程产生更复杂的过程。使用最广泛的面向过程的语言是通信顺序进程(CSP)。 |
SDLC的正式语言 |
| 在SDLC,正式的语言被用在两个阶段:需求和测试。 |
| 规范(需求分析阶段): |
| 规范是描述系统行为的过程及其所需的属性。正式规范语言描述可能包括功能行为的系统属性,时间行为,性能特征和内部结构,等[6]。 |
| Z, VDM和落叶松是用于指定顺序系统的行为,而其他正式的方法如CSP、CCS,状态图,时序逻辑,Lamport和I / O自动机,专注于指定并发系统的行为[7]。提高用于处理状态空间丰富,忘忧草是一种语言,由于并发处理的复杂性。 |
| 验证(测试阶段): |
| 验证是一个过程来证明或反驳一个系统的正确性对正式的规范或财产。验证的代码,有两个重要的形式:模型检查和定理证明[8]。 |
| 。在模型检查、系统的有限状态模型是构建和它的状态空间是机械地调查。两个著名的等效模型跳棋NuSMV和自旋。 |
| b。定理证明是另一个方法验证的规范或检查程序的正确性。模型中描述的系统模型的数学语言和所需的属性可以证明一个定理验证。这是机械化的逻辑证明。由定理验证检查的规范是写在一个数学符号。Z(发音“Zed”)是其著名的例子。 |
正式的方法的目标 |
| 正式的方法可以应用在软件开发生命周期的不同阶段。的基础上正式的方法的细节,有些目标可能会列出如下: |
| a。正式的方法支持创建规范,描述用户的真正需求,通常不与所要求的相同。这可以通过使用正式的方法,因为正式的含混标准规范和可能性来证明某些属性。 |
| b。正式的方法确保实现一个特定的软件以及硬件产品应满足规范要求。 |
| c。正式的方法基本上是关心的安全可靠关键系统开发和维护的时间和在预算之内。它增加诚信系统,系统的开发不仅是正确的,但知道是正确的。正式的方法作为证据,确保系统真正满足安全的需求,可靠性和正确性。 |
正式的方法的好处 |
| 在软件开发生命周期的早期活动即需求分析和规范,是最重要的。根据Standish混乱的报告[9],一半的项目失败发生由于需求规范差。最有效的使用正式的方法是在早期阶段。是有效的编写规范正式,而不是写一个非正式规范,然后翻译。检测不一致和不完整,有效分析尽早正式规范[10]。随着福利上面所讨论的,有各种各样的其他好处的讨论如下: |
| 测量的正确性:正式的方法的使用提供了一个衡量系统的正确性,而不是当前过程质量的措施。 |
| b。早期的缺陷检测:正式的方法可以应用于最早的设计工件,从而导致的早期检测和消除设计缺陷。 |
| c。保证正确性:正式的分析工具,如模型检查器通过该系统考虑所有可能的执行路径。如果有任何故障/错误的可能性,模型检查器会找到它的。在多线程系统,并发性是一个问题,正式的分析可以探索所有可能的交叉和事件排序。这种程度的报道是不可能通过测试。 |
| d。容易出错:正式描述迫使作家问各种各样的问题,否则将推迟到编码。这有助于减少错误发生期间或之后的编码。正式的方法有完整性的性质,即它涵盖所有方面的系统。 |
| e。抽象:如果软件或硬件产品的工作很简单,然后马上可以编写代码,但在大多数系统代码太大,一般需要系统的详细描述。正式规范,另一方面,是一种描述,是抽象的,精确的,在某种意义上完成。抽象允许人类读者理解大局的软件产品。 |
| f。严格的分析:描述的形式让我们执行严格的分析。正式描述通常写不同的观点,可以确定一个重要的属性如满足高层次的需求或建议设计的正确性。 |
| g。值得信赖:正式的方法提供的证据表明,需要在严格管制航空等行业的竞争。他们证明,提供具体的原因对产品的信任。 |
| h。有效的测试用例:从正式规范,我们可以直接从系统得到有效的测试用例规范。这是一个成本有效的方式来生成测试用例。 |
正式的方法的局限性 |
| 正式的方法在软件开发生命周期发挥重要的作用。然而,这些方法有一定的局限性。这些缺点限制了软件产品正式的方法的有效性。下面列出了一些正式的方法的局限性: |
| 规范的正确性:一般来说,实际用户需求可能不同于用户,和通常会随时间。在使用正式的方法,没有办法保证规范的正确性和完整性对用户的非正式的要求。然而;各种方法存在在文学的概率减少不正确的规范,但所有方法的出发点是一定非正式。一个永远不可能一定要正确地收集所有用户的需求。 |
| b。实现的正确性:很难确定一个给定的程序是否满足给定的规范。例如,当使用一个验证检查方法如Hoare逻辑,一个需要识别循环不变式,自动是不可能的。因此,它通常是不可能对现有程序的正确性证明尚未写的正确性证明。正确性证明只有可行的同时如果编程和证明。 |
| c。正确性的证明:证明正确性发挥重要作用在正式的方法。正确性证明增加程序的概率是正确的。通常不能保证规范以及实现的正确性。证明的主要问题在于证据的创建。有时候,有可能证明正确性可能会失败。可能原因的正确性的证明一个实现对其规范可能会失败[11]: |
| 一)程序不正确,需要修改。 |
| b)程序是正确的,但正确性证明尚未发现。 |
| c)程序是正确的,但是没有正确性证明。 |
| 处理复杂的语言特性:正式的语义定义最重要的语言结构和软件系统的组件不可用或太复杂是有用的。对于证明程序的属性,这些结构或组件将是必需的。有些复杂的数据结构,指针,人机界面(HCI)和错误消息等。一般来说,一半以上任何真正的生产系统由人机交互的代码和错误消息。 |
| b。的技术环境:一个正式的描述程序应该包含一个描述一个程序是配合硬件和操作系统的规范下为了证明程序的正确性。通常这样一个正式的描述往往是不可用的工业软件开发中使用的技术环境。问题恶化,这样一个正式的描述必须采取一个非常具体的形式取决于所使用的正式方法(例如作为理论用于定理验证)。这适用于开发环境和生产环境。至于开发环境,使用的编程语言的正式定义及其语义在编译器中实现是必要的。 |
| 引入的额外的并发症等方面的环境: |
| 一)舍入误差与浮点数计算。这些都是正式的方法的原因通常不应用于数值算法。 |
| b)大小的限制。 |
不是通过正式的方法来解决问题 |
| 有一些问题没有解决的正式方法。这些是下面讨论: |
| 创造力:正式的方法是描述和分析。他们不认为是创造性的。在现实中,只有正式的方式描述和分析设计。没有一个正式的设计过程。为了开发一个真正的系统,我们必须将正式的方法与其他方法相结合。 |
| b。软件产品质量:正式的方法处理软件本身和它的文档。其他软件产品的重要组成部分,如培训、客户支持、维护或安装的软件,需要单独处理。这些组件及其质量一起形成一种高质量的产品。正式的方法不提供软件产品质量。因此,大多数成功的软件产品提供商必须把大量的精力解决所有相关方面的软件产品。 |
| c。软件系统和他们的社会和生态环境:软件系统通常需要输入从外部环境。这些输入可能不是可预测的。这明显的忽视问题通常创建正确的规范发展中存在的问题和决定哪些行为是正确的。正式的方法有助于对这方面的软件系统。 |
未来的研究方向 |
| 调频(正式的方法)是一个非常活跃的研究领域,各种各样的方法和数学模型。可用在当前的场景中,没有任何一个方法,满足所有安全相关的需求构建一个安全的正式规范。研究者和实践者不断工作在这一领域,从而获得使用正式的方法的好处。此外,未来的工作需要完成下列研究领域的代表在图7.1)。 |
| 。工作可能会发起建立一个正式的方法,结合其他各种好处的方法集中在构建安全的正式规范。 |
| b。工作可能做降低成本在SDLC的不同阶段使用正式的方法。c。识别和解决各种正式规范验证工具。 |
| d。进一步的研究是需要利用组合多个抽象的数学理论。 |
| e。需要扩大规模的符号形式方法和工具支持,使它容易使用。f。工作可能开始优化方法和工具寻找错误标识系统的正确性。 |
| g。研究可能进行摊销的成本在许多使用的方法或工具。应该有可能获得受益于一个规范在项目的生命周期:几个点上的设计分析、代码优化和测试。 |
| h。工作可能会开始开发一个工具,可以帮助了解如何编写方法、规范、模型、理论,和证明。 |
| 我。一个新的数学模型也可能为检查开发需求规范的完整性和逻辑一致性 |
 |
结论 |
| 本文提出了正式的方法的不同方面。在软件开发中出现的主要缺陷由于糟糕的需求分析。此外,正式的方法只是解决方案的一部分需求分析相关的问题和成功关键取决于整合成一个更大的过程。本文有助于研究者/ s和开发人员理解的潜在效用通常面临正式的方法和挑战做出正式的实用方法。重要的需要在软件开发中需要的所有方法是更具体的需求阶段,因为需求是整个软件的基本构建块可以建造。这项工作激励软件工程师将安全需求阶段,这样可以实现产品质量。 |
确认 |
| 作者感谢Manish Gupta先生,总理Jagan纳大学,迪帕克·古普塔先生,副董事长Jagan Nath Gupta纪念教育社会,V.K. Agarwal教授,副校长,Jagan纳大学教授和屈服强度Shishodia,副校长,Jagan纳大学,斋浦尔,为本研究提供鼓励和支持工作。 |
引用 |
|
