The Maude strategy language
为控制Maude规约中重写规则的非确定性以兼顾多方面需求，研究提出Maude策略语言，介绍其语义、从Maude反射实现到C++集成实现的演进及多领域应用。
2024-02-01 cs.LO
A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
LIPN CNRS UMR 7030 Université Sorbonne Paris Nord（巴黎北大学国家科学研究中心联合研究实验室）；Pohang University of Science and Technology（韩国科学技术院）；University of Oslo（奥斯陆大学）
本文提出了一种用于参数时间Petri网的形式化分析与参数综合框架，利用重写逻辑与SMT求解器实现精确语义分析，通过符号可达性方法实现参数综合，实验表明方法在多个方面优于现有工具。
2024-09-12 cs.LO
Rewriting Logic Semantics of a Plan Execution Language
计划执行交换语言（英语：Plan Execution Interchange Language，缩写：PLEXIL）是一种由NASA开发的同步语言，用于支持自主航天器操作。在本文中，我们提出了一个重写的逻辑语义PLEXIL在Maude，一个高性能的逻辑引擎。重写逻辑语义本身就是语言的形式解释器，可以用作PLEXIL执行程序实现的语义基准。在Maude中的实施还有一个额外的好处，即为PLEXIL设计人员和开发人员提供Maude提供的所有正式分析和验证工具。PLEXIL语义在重写逻辑中的形式化提出了一个有趣的挑战，由于语言的同步性和定义其语义的优先级规则。为了克服这个困难，我们提出了一个通用的程序，用于模拟同步集关系重写逻辑是健全的，确定性的关系，完成。我们还报告了两个问题，在设计层面上的原始PLEXIL语义确定的帮助下，在Maude的可执行规范。
2010-02-15 cs.LO cs.PL
Specification and Verification of Distributed Embedded Systems: A Traffic Intersection Product Family
分布式嵌入式系统（DES）不再是例外;它们是许多应用领域的规则，如航空电子，汽车工业，交通系统，传感器网络和医疗设备。由于状态空间爆炸和实时特性的需要，形式化的DES规范和验证具有挑战性。本文报告了一个广泛的基于行业的案例研究，涉及DES产品系列的行人和汽车4路交通路口，其中自主设备通过异步消息传递进行通信，而无需集中控制器。已使用实时Maude及其模型检验功能正式验证了需求文档中非正式规定的所有安全需求和活性需求。
2010-09-22 cs.LO
Model checking strategy-controlled systems in rewriting logic
本文针对 Maude 内置 LTL 模型检测器无法验证策略控制规约的问题，提出策略感知扩展，并结合表达力分析、应用示例和性能比较验证其有效性。
2024-01-15 cs.LO
Distributed Real-Time Emulation of Formally-Defined Patterns for Safe Medical Device Control
医疗器械及其互操作的安全性是一个尚未解决的问题，导致严重的，有时是致命的事故，病人令人震惊的频率。形式化方法，特别是支持高度可重用和可证明安全的模式，可以实例化到许多设备实例，可以在这方面提供帮助。然而，这仍然留下了一个问题，即如何从逻辑时间上的正式规范传递到可执行的仿真，这些仿真可以在物理时间上与其他设备以及患者和/或医生行为的模拟进行互操作。这项工作提出了一种基于规范的方法，其中虚拟仿真环境可以很容易地从正式规范在实时的【形】Maude开发，并可以支持与其他真实设备和仿真模型的交互。这种一般的方法进行了详细的解释，并说明了两个具体的情况下，这两个实例的一个共同的安全正式模式：一个场景涉及到一个可证明的安全起搏器与模拟心脏的相互作用;另一个涉及到一个安全的控制器的相互作用，病人诱导镇痛与一个真正的注射泵。
2010-09-22 cs.LO cs.SE
Dist-Orc: A Rewriting-based Distributed Implementation of Orc with Formal Analysis
Orc是一种服务编排理论，允许分布式和定时计算的结构化编程。已经提出了几种形式语义的Orc，包括重写逻辑语义的作者开发的。Orc在Java中也有一个完全成熟的实现，具有函数式编程特性。然而，与大多数分布式语言的描述一样，Orc的形式语义和其实现之间存在相当大的差距，因为：（i）Orc中的程序不容易仅通过使用Orc的形式语义在分布式实现中部署，以及（ii）它们不容易在分布式Orc实现的级别上进行形式分析。在这项工作中，我们克服了Orc的问题（i）和（ii）。具体来说，我们描述了一种基于重写逻辑和Maude的实现技术，大大缩小了这一差距。这种技术的启用特性是Maude通过TCP套接字支持外部对象。我们描述了如何使用套接字来实现Orc站点调用和返回，并为Orc表达式和站点提供实时定时信息。然后，我们将展示如何在所得到的分布式实现的Orc程序可以正式分析在一个合理的抽象层次，通过定义一个抽象的时间模型和套接字通信基础设施，并讨论的假设下，分析可以被认为是正确的。最后，通过一个实例说明了分布式实现和形式化分析方法。
2010-09-22 cs.DC cs.LO cs.PL
Unified Opinion Dynamic Modeling as Concurrent Set Relations in Rewriting Logic
提出基于并发集合关系和重写逻辑的统一框架，用于指定、模拟和分析动态意见模型的社会交互系统，并在Maude中实现可执行理论与模型检查。
2024-02-14 cs.LO
Technical Report: Time-Bounded Resilience
本文研究了$η$-简单递进规划场景类中时间有界弹性问题的计算复杂度，证明了其在具有$n$个更新时对多项式层次结构PH的$Σ^P_{2n+1}$类是完全的，并使用Maude工具进行了实验验证。
2024-06-02 cs.LO
Using Formal Methods for Autonomous Systems: Five Recipes for Formal Verification
形式方法是用于软件设计和工程的基于数学的技术，它能够对系统的行为进行明确的描述和推理。自主系统使用软件在没有人类控制的情况下做出决策，通常嵌入在机器人系统中，通常是安全关键的，并且越来越多地被引入日常环境中。自治系统需要健壮的开发和验证方法，但形式化方法的实践者经常被问到：为什么要使用自治系统的形式化方法？为了回答这个问题，这份立场文件描述了从文献中收集的五个配方，用于正式验证自治系统的各个方面。配方的例子是如何形式化方法可以成为一个有效的工具，自主系统的开发和验证。在设计过程中，它们可以明确地描述需求;在开发过程中，可以根据需求验证正式规范;可以从验证的规范合成软件组件;可以在运行时监控行为并与原始规范进行比较。现代形式化方法通常包括高度自动化的工具支持，这使得能够对系统的状态空间进行详尽的检查。本文认为，形式化方法是一个强大的工具，与其他强大的软件工程技术的发展技术的剧目安全自治系统。
2021-07-28 cs.LO cs.SE
Proceedings First Workshop on Causal Reasoning for Embedded and safety-critical Systems Technologies
自动因果关系分析，故障定位，事件解释，问责制和责备的正式方法已经由几个社区独立提出-特别是人工智能，并发，基于模型的诊断，正式方法。在过去几年中，关于这些专题的工作大大加快了速度。CREST的目标是汇集和促进来自不同社区的研究人员之间的交流，并介绍和讨论该领域的最新进展和新想法。研讨会的程序包括一组邀请和贡献的演示文稿，说明不同的技术，因果关系分析和故障定位的应用。该计划由两个主题演讲组成。Hana Chockler（国王学院）的主旨发言提供了一个广泛的视角，探讨了基于Halpern和Pearl对实际因果关系的定义的因果推理在从形式化验证到法律推理等各种应用领域的应用。Chao Wang（弗吉尼亚理工大学）的主题演讲集中在调试和验证并发程序的基于约束的分析技术。研讨会论文涉及成分因果关系分析和广泛的因果推理应用，如概率模型的调试，问责制和责任，基于刘易斯反事实的实践中的危险分析，以及故障定位和修复。
2016-08-26 cs.AI cs.LO cs.SE
A Rewriting Logic Approach to Stochastic and Spatial Constraint System Specification and Verification
本文讨论的问题，指定，模拟和验证反应系统重写逻辑。它提出了一个可执行的语义概率，时间和空间并发约束编程-这里称为随机和空间并发约束系统（SSCC）-在重写逻辑语义框架。该方法是基于一个增强和广义模型的并发约束规划（CCP）的计算层次空间可以分配给属于代理。可执行语义忠实地表示和操作捕捉高度并发的性质，不确定的行为，空间和认知特征的反应系统与信息流。在SSCC中，定时属性（由随机持续时间表示）可以与进程相关联，并且还支持排他性和独立的概率选择。利用Maude系统中的SMT求解技术，实现了SSCC的底层约束系统，包括整数和实数上的无量词公式。这导致了一个完全可执行的实时符号规范，可用于定量分析的统计模型检验的形式。SSCC的主要特点和能力说明了整个文件的例子。这一贡献是一个更大的研究工作的一部分，旨在提供正式的分析技术和工具，数学上建立在CCP的方法，研究界。
2022-11-03 cs.LO
Is your software on dope? Formal analysis of surreptitiously "enhanced" programs
通常，软件制造商采用验证或测试来确保嵌入在设备中的软件满足其主要目标。然而，这些天来，我们面临的情况是，经济或技术的原因可能会使制造商成为有兴趣的软件稍微偏离其主要目标的可疑原因。例子包括锁定战略和汽车行业的$\mathrm{NO}_x$排放丑闻。这种现象我们称之为软件兴奋剂。随着越来越多的软件被嵌入到日常使用的设备中，它变得越来越普遍。本文的主要贡献是提供了一个简单但可靠的形式化定义的层次结构，可以区分程序是干净的还是掺杂的。此外，我们表明，这些特征提供了一个直接的框架，通过使用现有的验证技术进行分析。我们通过在顺序程序上应用自组合和在反应模型上应用HyperLTL公式的模型检验来验证这一点。
2017-02-15 cs.LO
Proceedings of the Sixth Working Formal Methods Symposium
我们很高兴地介绍在“Al. I.”举行的第六届工作形式方法研讨会（从2022年开始）的论文。2022年9月19日至20日，罗马尼亚雅西大学。从旨在汇集研究人员和从业者谁工作的正式方法，通过贡献新的理论成果，方法，技术和框架，和/或使正式方法的工作，通过创建或使用软件工具，应用理论的贡献。该计划委员会选择了五个贡献和四个邀请演讲，其中一个与第28届逻辑，语言，信息和计算研讨会（WoLLIC 2022）共享。两个贡献处理匹配逻辑，一个表达逻辑框架，程序设计语言和其他逻辑的正式定义可以嵌入。其他贡献涉及分布式系统，多代理系统和教学正式的方法。邀请的会谈目前的工作与这些主题大致一致。
2022-09-19 cs.LO cs.PL cs.SE
On the automated verification of web applications with embedded SQL
大量Web应用程序基于关系数据库以及程序（通常是脚本），该程序使用户能够通过嵌入式SQL查询和命令与数据库交互。在本文中，我们介绍了一种方法，这种系统连接数据库理论的主流程序分析的形式化自动验证。我们确定了一个片段的SQL，它捕获的行为，在我们的案例研究中的查询，是算法可判定的，并有利于建设最弱的先决条件。因此，我们可以将SQL查询的分析集成到程序分析工具链中。为此，我们实现了一个新的决策过程的SQL片段，我们介绍。我们证明了我们的研究结果与三个案例研究，一个Web管理员，一个简单的防火墙，和一个会议管理系统的实用性。
2016-10-06 cs.LO
Delayed Constraints in Narrowing for the Logic-Based Analyses of Real-Time Systems
VRAIN, Universitat Politècnica de València（瓦伦西亚理工大学）；LIPN, CNRS UMR 7030, Université Sorbonne Paris Nord（索邦巴黎北大学）
研究实时系统形式分析中无穷性的两个维度，提出基于归约的验证方法，整合重写、归约及约束存储等技术，引入折叠机制确保终止，通过验证协议评估，能统一支持多种实时模型分析，为实时重写理论符号验证提供基础。
2026-07-24 cs.LO cs.PL cs.SC
Proceedings 2nd International Workshop on Causal Reasoning for Embedded and safety-critical Systems Technologies
Northern Arizona University（北亚利桑那大学）；University of Konstanz（康斯坦茨大学）
本文探讨了复杂嵌入式和安全关键系统中因果推理的方法，旨在促进不同领域研究者之间的交流，以提升关键系统故障根本原因分析的科学性。
2017-10-08 cs.LO cs.SE cs.SY
Equivalence Checking in Embedded Systems Design Verification
在这份报告中，我们专注于嵌入式系统的建模和形式化验证相关的一些方面。已经提出了许多模型来表示嵌入式系统。这些模型涵盖了广泛的风格，特点和应用领域，包括有限状态机，数据流图，通信过程和Petri网的扩展。在本报告中，我们使用了PRES+模型（基于Petri网的嵌入式系统表示）作为经典Petri网模型的扩展，该模型捕获了嵌入式系统的并发性和时序行为;它允许系统在不同的抽象级别中具有代表性，并通过允许令牌携带信息来提高表达能力。如上所述，使用PRES+建模可能便于指定输入行为，因为它支持并发性。然而，据我们所知，文献中没有报道PRES+模型的等价性检查方法。相反，存在FSMD模型的等价性检查。作为第一步，因此，我们试图设计一个算法，将PRES+模型FSMD模型。
2010-08-20 cs.FL cs.LO
Formal verification of a time-triggered hardware interface
我们提出了一个时间触发的硬件接口的正式证明。该设计实现了汽车嵌入式系统FlexRay标准规定的位时钟同步机制。该设计是在门级描述。它可以被翻译成Verilog并在FPGA上进行综合。证明是基于异步通信的一般模型，并结合了互动的定理证明在伊莎贝尔/HOL和自动模型检查使用NuSMV连同一个模型简化过程，IHaVeIt。我们的异步通信的一般模型定义了模拟和数字关注点之间的明确分离。这种分离使得定理证明和模型检查的有效方法相结合。在Isabelle/HOL逻辑中形式化了模拟现象。使用IHaVeIt自动分析门级硬件。我们的证明揭示了位时钟同步机制的一个关键参数的正确值。我们的主要定理证明了功能的正确性以及传输的最大循环数。
2011-03-11 cs.LO
Proceedings Second Workshop on Formal Methods for Autonomous Systems
自治系统是高度复杂的，对形式化方法的应用提出了独特的挑战。自主系统在没有人为干预的情况下运行，并且通常嵌入在机器人系统中，以便它们可以与现实世界进行交互。因此，它们表现出安全关键，网络物理，混合和实时系统的属性。FMAS的目标是汇集正在使用正式方法解决自治系统独特挑战的领先研究人员，以展示最近和正在进行的工作。我们感兴趣的是使用形式化方法来指定，建模或验证自主或机器人系统;全部或部分。我们也有兴趣在成功的工业应用和潜在的未来方向，这种新兴的应用正式的方法。
2020-12-02 cs.AI cs.LO cs.RO
Equivalence Checking in Embedded Systems Design Verification using PRES+ model
本文主要研究嵌入式系统的建模和形式化验证。已经提出了许多模型来表示嵌入式系统。这些模型涵盖了广泛的风格，特点和应用领域，包括有限状态机，数据流图，通信过程和Petri网的扩展。在本报告中，我们使用了PRES+模型（基于Petri网的嵌入式系统表示）作为经典Petri网模型的扩展，该模型捕获了嵌入式系统的并发性和时序行为;它允许系统在不同的抽象级别中具有代表性，并通过允许令牌携带信息来提高表达能力。如上所述，使用PRES+建模可能便于指定输入行为，因为它支持并发性。然而，据我们所知，文献中没有报道PRES+模型的等价性检查方法。相反，存在FSMD模型的等价性检查。因此，作为第一步，我们寻求设计一种算法来将PRES+模型转换为FSMD模型，并且我们寻求在现实生活中的示例上手动执行我们的算法，并且我们必须将两个版本的PRES+模型转换为FSMD模型。然后使用现有的等价性检查器，我们已经检查了两个FSMD模型之间的等价性。
2010-10-24 cs.FL cs.LO
