XiaoMi-AI文件搜索系统
World File Search SystemFORMEDICIS
正式开发用于 ARINC 661 的多用途交互式应用程序 (MPIA)
摘要。本文介绍了我们使用形式化方法开发符合 ARINC 661 规范标准的人机界面 (HMI) 的经验，该界面可用于交互式驾驶舱应用程序。此开发依赖于我们在 FORMEDICIS 1 项目中提出并正式定义的 FLUID 建模语言。FLUID 包含指定 HMI 所需的基本功能。为了开发多用途交互式应用程序 (MPIA) 用例，我们遵循以下步骤：使用 FLUID 语言编写 MPIA 的抽象模型；此 MPIA FLUID 模型用于生成 Event-B 模型，以检查功能行为、用户交互、安全属性以及与域属性相关的交互；Event-B 模型还用于使用 ProB 模型检查器检查时间属性和可能的情况；最后，使用 PetShop CASE 工具将 MPIA FLUID 模型转换为交互式协作对象 (ICO)，以验证动态行为、视觉属性和任务分析。这些步骤依赖于不同的工具来检查内部一致性以及可能的 HMI 属性。最后，使用 FLUID 对 MPIA 案例研究进行正式开发并将其嵌入到其他正式技术中，证明了我们在 FORMEDICIS 项目中定义的方法的可靠性、可扩展性和可行性。
ARINC 661 的多用途交互式应用程序 (MPIA)
摘要。本文介绍了我们使用形式化方法开发符合 ARINC 661 规范标准的人机界面 (HMI) 的经验，该界面可用于交互式驾驶舱应用程序。此开发依赖于我们在 FORMEDICIS 1 项目中提出并正式定义的 FLUID 建模语言。FLUID 包含指定 HMI 所需的基本功能。为了开发多用途交互式应用程序 (MPIA) 用例，我们遵循以下步骤：使用 FLUID 语言编写 MPIA 的抽象模型；此 MPIA FLUID 模型用于生成 Event-B 模型，以检查功能行为、用户交互、安全属性以及与域属性相关的交互；Event-B 模型还用于使用 ProB 模型检查器检查时间属性和可能的情况；最后，使用 PetShop CASE 工具将 MPIA FLUID 模型转换为交互式协作对象 (ICO)，以验证动态行为、视觉属性和任务分析。这些步骤依赖于不同的工具来检查内部一致性以及可能的 HMI 属性。最后，使用 FLUID 对 MPIA 案例研究进行正式开发并将其嵌入到其他正式技术中，证明了我们在 FORMEDICIS 项目中定义的方法的可靠性、可扩展性和可行性。