通用唯一识别码
通用唯一识别码（，缩写：UUID）是用于计算机体系中以识别信息的一个128位标识符。 UUID按照標準方法生成時，在實際應用中具有唯一性，且不依赖中央机构的注册和分配。UUID重复的概率接近零，可以忽略不计。 因此，所有人都可以自行建立和使用UUID，而且幾乎可以確定其不會與既有的識別碼重複。也因為如此，在不同地方產生的UUID可以使用於同一個資料庫或同一個頻道中，而且幾乎不可能重複。 UUID的應用相當普遍，許多計算平台都提供了對於生…
标签：#形式方法
共 24 篇文章
形式语义学
在计算理论中，形式语义学是关注计算的模式和程序设计语言的含义的严格的数学研究的领域。 语言的形式语义是用数学模型去表达该语言描述的可能的计算来给出的。 形式语义学（formal semantics），是程序设计理论的组成部分，以数学为工具，利用符号和公式，精确地定义和解释计算机程序设计语言的语义，使语义形式化的学科。 提供程序设计语言的形式语义的方法很多，其中主要类别有： 指称语义学，着重于语言的执行结果而非过程，包括域理论； 操作语义…
集合论
交集的文氏圖]] 集合論（）或稱集論，是研究集合（由一堆抽象对象構成的整體）的數學理論，包含集合和元素（或稱為成員）、關係等最基本數學概念。在大多數現代數學的公式化中，都是在集合論的語言下談論各種数学对象。集合論、命題邏輯與謂詞邏輯共同構成了數學的公理化基礎，以未定義的「集合」與「集合成員」等術語來形式化地建構數學物件。 現代集合論的研究是在1870年代由俄国数学家康托爾及德國数学家理察·戴德金的樸素集合論開始。在樸素集合論中，集合是當…
自動化定理證明
中的一個證明例子]] 自動化定理證明（，簡稱ATP）是自動推理（AR）體系中發展最成熟的子領域，其目的是使用電子計算機程序來進行數學定理的證明。對於不同的公理系統，自動定理證明器能夠推論出一個定理在此系統下是正確的、不可證明的還是錯誤的。 邏輯基礎 形式化邏輯的根源可追溯至亞里士多德，但現代邏輯和形式化數學的發展主要在19世紀末至20世紀初。戈特洛布·弗雷格的《概念文字》（1879年）引入了完備的命題邏輯和本質上是現代謂詞邏輯的系統。伯…
聯合國大學澳門研究所
聯合國大學澳門研究所（；, ），前身為聯合國大學國際軟件技術研究所（；, ）與聯合國大學計算與社會研究所（，縮寫UNU-CS），联合国大学下属机构之一，始创于1992年，為聯合國、中國、澳門及葡萄牙政府協議下成立。主要研究方向是形式化方法的理论和应用以及电子政务。研究所位于澳门。 於2015年，聯合國大學計算與社會研究所所長Michael L. Best全責重新建立新的研究所，由聯合國大學計算與社會研究所承續並取代聯合國大學國際軟件技術…
统计静态时序分析
传统的静态时序分析（Static Timing Analysis，STA）长期以来是数字电路设计中的常用分析算法。但半导体器件与互连的变异性增加，带来若干传统（确定性）STA无法处理的问题。由此催生了大量关于统计静态时序分析（Statistical Static Timing Analysis，SSTA）的研究。SSTA用概率分布替代门与互连的确定性时延，输出的是电路可能结果的分布，而非单一结果。 与传统STA的比较 确定性STA之所以…
指称语义
在计算机科学中，指称语义（）是通过构造表达其语义的（叫做指称(denotation)或意义的）数学对象来形式化计算机系统的语义的一种方法。编程语言的形式语义的其他方法包括公理语义和操作语义。指称语义方式最初开发来处理一个单一计算机程序定义的系统。后来领域扩展到了由多于一个程序构成的系统，比如网络和并发系统。 指称语义起源于 克里斯托弗·斯特雷奇 和 Dana Scott 在1960年代的工作。在 Strachey 和 Scott 最初开…
抽象释义
在计算机科学中，抽象解释（abstract interpretation，在上下文明確時可簡稱AI）是基于在有序集合特别是格上的单调函数，计算机程序的语义的可靠逼近理论。它可以被看作对计算机程序的部分执行，获取关于它的语义信息（比如，控制结构、数据流）而不进行所有计算。 它的主要具体应用是静态分析，关于计算机程序的可能执行的信息的自动提取；这种分析有两个主要用途: 在编译器内部，分析程序来确定特定优化或变换是否是可适用的； 针对缺陷类的…
高低階
高階、低階（）是在邏輯學及計算機科學相關領域中，與「推論的一種技術：抽象化」有關的概念。由於不同的人類在思考時，偏好「將特定命題抽象化或具體化成自己容易思考的程度」。「高階、低階」就是指稱「命題抽象化的程度」。命題越抽象，就越高階。越具體而不抽象，就越低階。 「高階、低階」在權能的概念裡，指稱的是權能的大小及多寡。
静态时序分析
静态时序分析（），或称静态时序验证，是电子工程中，对数字电路的时序进行计算、预计的工作流程，该流程不需要通过输入激励的方式进行仿真。 传统上，人们常常将工作时钟频率作为高性能的集成电路的特性之一。为了测试电路在指定速率下运行的能力，人们需要在设计过程中测量电路在不同工作阶段的延迟。此外，在不同的设计阶段（例如逻辑综合、布局、布线以及一些后续阶段）需要对时间优化程序内部进行延迟计算（）。尽管可以通过严格的SPICE电路仿真来进行此类时间测…
斷言 (程式)
在程式設計中，斷言（assertion）是一種放在程式中的一階邏輯（如一個結果為真或是假的邏輯判斷式），目的是為了標示與驗證程式開發者預期的結果－當程式執行到斷言的位置時，對應的斷言應該為真。若斷言不為真時，程式會中止執行，並給出錯誤訊息。 例如，以下的程式包括二個斷言： x := 5; {x > 0} x := x + 1 {x > 1} x > 0及x > 1，當程式執行到二個斷言對應的位置時，斷言的內容均為真。 程式設計者可以用斷…
模型检测
在计算机科学领域，模型检测或属性检测是一种用于验证系统的有限状态模型是否满足给定规范（即正确性）的方法。这种方法通常应用于硬件或软件系统；在此类系统中，规范不仅包含安全性需求（例如避免导致系统崩溃的状态），同时也包含活性需求（例如避免活锁现象）。 为了能够通过算法解决此类问题，系统的模型及其规范均需使用精确的数学语言进行形式化表述。为此，该问题被转化为逻辑范畴下的任务，即验证某个特定的结构是否满足给定的逻辑公式。这一通用概念适用于多种逻…
生命攸關系統
生命攸關系統（life-critical system）或安全攸關系統（safety-critical system）也稱為生命關鍵系統或安全關鍵系統，是指若系統失效或誤動作，可能會產生以下後果的系統： 人員重傷或死亡 設備的嚴重毀損 環境的危害 安全相關系統（Safety-involved systems）類似安全關鍵系統，但安全性要求略低。若只有此系統失效，不會造成人員傷亡、設備的嚴重毀損或者環境危害等重大。安全相關系統的誤動作只有…
行为时序逻辑
行为时序逻辑（）是由莱斯利·兰伯特（Leslie Lamport）发展的用于规范和推理并发自反应系统的时间逻辑。 主要应用于计算机科学，程序验证。
动态时序验证
动态时序验证（）是指对专用集成电路的一种验证过程，它被用来检查电路是否能够以足够快的速率在指定的时钟频率下正常。将用于集成电路综合过程的设计文件进行仿真，动态时序验证得以进行。该过程与静态时序分析相对应，后者与动态时序验证有着相似的目标，但是它并不需要对集成电路的实际功能进行仿真。 参考文献
軟體驗證及確認
在軟體專案管理、軟體工程及軟體測試中，驗證及確認（，簡稱V&V）是指檢查軟體是否符合規格及其預期目的的程序。驗證及確認也被視為一種軟體品質管理，是软件开发过程的一部份，一般歸類在軟體測試中。 驗證及確認有時會由公正的第三方單位進行，此情形下的驗證及確認稱為獨立驗證及確認，簡稱IV&V。 定義 確認（validation）的目的是檢查產品設計是否符合其預期的目的，軟體確認的目的是檢查軟體是否符合使用者的需求而言，可以由或是其他方式的審查來…
循环不变量
在计算机科学中，循环不变式（loop invariant，或循环不变量、循环不变条件，也有译作循环不变性），是一组在循环体内、每次迭代均保持为真的性质（表达式），通常被用来证明程式或伪码的正确性（有时但较少情况下用以证明算法的正确性）。简单说来，“循环不变式”是指在循环开始和循环中，每一次迭代时为真的性质。这意味着，一个正确的循环体，在循环结束时“循环不变式”和“循环终止条件”必须同时成立。 由于循环和递归的相通，证明带有不变式的循环的…
形式验证
在计算机硬件（特别是集成电路）和软件系统的设计过程中，形式验证的含义是根据某个或某些形式规范或属性，使用数学的方法证明其正确性或非正确性。 解释 软件测试无法证明系统不存在缺陷，也不能证明它符合一定的属性。只有形式化验证过程可以证明一个系统不存在某个缺陷或符合某个或某些属性。系统无法被证明或测试为无缺陷，这是因为不可能形式地规定什么是「没有缺陷」。所有可以做的，就是证明一个系统没有任何可以想到的缺陷，并且满足所有的使系统符合功能要求的和…
形式化方法
形式化方法，中文也稱形式方法、正規方法。在计算机科学和软件工程领域，形式化方法是基于数学的特种技术，适合于软件和硬件系统的描述、开发和验证。将形式化方法用于软件和硬件设计，是期望能够像其它工程学科一样，使用适当的数学分析以提高设计的可靠性和強健性。但是，由于采用形式化方法的成本高意味着它们通常只用于开发注重安全性的高度整合的系统。 参考文献
時間分割測試
TPT（Time Partition Testing 分时段测试，以下简称 TPT）是一种采用分时段测试方法进行软件测试和软件验证的自动化工具软件，主要应用于嵌入式系统中基于模型或者代码的模块测试，集成测试，系统测试和回归测试。 TPT的主要功能： 搭建测试模型和测试用例 各种系统平台，如Matlab/Simulink, ASCET, Targetlink, C/Code，CAN, LIN，和各个开发阶段，如MiL， SiL, PiL,…