《ACM Transactions on Embedded Computing Systems》：Introduction to the Special Issue on Specification and Design Languages
编辑推荐：
国际学术会议FDL 2022和2023届聚焦软硬件系统开发的语言、工具及方法，涵盖物联网、嵌入式系统等领域，特别刊载六篇论文，涉及硬件设计语言、嵌入式系统变换、物联网验证、多类型逻辑、GPU架构优化及边缘计算验证等方向。
规范与设计语言论坛（FDL）是一个国际性活动，学者和公司代表在此交流与软件和硬件系统开发相关的语言、工具及技术的成果、经验、进展和新趋势。目标系统包括信息物理系统、分布式系统、实时系统、嵌入式系统、机电一体化系统、物联网系统以及反应式系统。
FDL涵盖以下四个非限制性的科学领域：
—
语言： 对软件领域特定语言、执行平台、资源分配、环境描述、契约定义、抽象模型及其细化方法感兴趣，同时关注相关的设计方法、框架和工具。
—
语义学： 关注形式化定义、编译器、解释器、类型系统、抽象/细化技术，以及这些概念的规范框架、建模方法和模型转换的新途径。
—
验证与分析： 重点研究创新的静态分析方法、测试技术、调试工具、模型检查技术、基于机器学习的分析方法以及设计空间探索技术，同时涉及相关的模型、工具和框架。
—
仿真： 关注创新的仿真技术、虚拟原型技术、数字孪生技术、协作仿真技术以及运行时抽象/细化技术，特别关注仿真的效率和正确性及其所依赖的工具和框架。
2022年规范与设计语言论坛（FDL 2022）于9月14日至16日在奥地利林茨举行，包括三场主题演讲（弗莱堡大学的Armin Biere教授、英飞凌科技的Rainer Findenig博士、慕尼黑应用科技大学的Stefan Wallentowitz教授）、五场技术会议、两场教程、一个小组讨论会和一个博士论坛。2023年论坛（FDL 2023）于9月13日至15日在意大利都灵举行，包括两场主题演讲（英飞凌科技的Hayri Hasou、慕尼黑工业大学的Robert Wille教授）、七场技术会议、两场教程、一个博士论坛以及一个与会议同时进行的博士培养项目。这两场活动都吸引了大量参与者，包括研究人员、从业者、学生和公司代表。
为了更深入地探讨部分论文内容并扩大读者群体，我们向《ACM TECS》杂志发出了征稿邀请。最终共有六篇论文入选，这些论文或是新提交的稿件，或是对FDL 2022或FDL 2023已接受论文的补充内容。
以下是本期特刊收录的论文列表：
“
PEak: 一种统一的硬件设计与验证工具”作者：C. Donovick, R. Daly, L. Truong, P. Raina, P. Hanrahan, C. Barrett。本文介绍了一种开源硬件设计与规范语言PEak，它整合了功能模型、形式化规范和RTL代码，提升了设计效率和验证效果。PEak弥合了灵活的硬件描述语言与静态指令集规范语言之间的差距，支持早期设计空间探索。
“
弥合抽象差距：基于规则的嵌入式系统转换设计方法”作者：F. Bahrami, R. Jordao, I. Sander, I. S?derquist。本文提出了一种针对异构多处理器嵌入式系统的基于规则的转换设计方法。该方法结合了RAMP视图（需求、应用模型、平台模型和映射决策）以及统一的抽象图表示，通过模式匹配技术和概念验证工具自动识别可应用的转换方案，从而丰富设计空间并促进有效的设计与平台协同探索。
“
SMrCaIT演算的证明系统”作者：N. Chen, H. Huibiao。本文为SMrCaIT演算构建了一个证明系统，该演算用于描述物联网系统的安全性、移动性和实时特性。基于此演算，文章提出了一种基于时间扩展的Hoare逻辑的证明系统，并通过车辆自组织网络（VANET）和多无人机场景验证了其有效性。
“
MLTL多类型逻辑：适用于信息物理系统的类型化逻辑”作者：G. Hariharan, B. Kempa, T. Wongpiromsarn, P. Jones, K. Rozier, Kristin。MLTLM是对任务时序线性逻辑（Mission-time Linear Temporal Logic）的扩展，能够清晰直观地表达不同类型信号下的信息物理系统需求。该逻辑保留了MLTL的简洁性和语言到形式的对应关系，支持异构信号处理，并在资源受限的硬件环境中提升效率。文章通过多类型示例、完整证明以及与MLTL的比较结果进一步阐述了其优势。
“
无缓存处理单元网格的混合级建模与评估”作者：Vivek Govindasamy, Rainer D?mer。本文提出了一种名为“处理单元网格（GPC）”的可扩展并行架构，使用SystemC TLM-2.0在指令级和功能层对网格进行建模，实现高效准确的仿真。通过测试流处理应用并分析软件优化，证明GPC显著减少了执行时间，尤其是在主内存竞争方面优于传统共享内存处理器。
“
基于断言的机器人应用边缘-云协同验证平台”作者：S. Germiniani, N. Bombieri, F. Lumpp, G. Pravadelli, Graziano。本文提出了一种用于自主机器人的运行时断言验证（ABV）平台，该平台能够从信号时序逻辑规范中生成验证规则，并动态地在边缘和云资源之间迁移这些规则。尽管ABV能有效检测复杂机器人系统中的错误，但其运行时开销可能影响资源受限架构的性能。本文通过监控规则生成、ROS兼容集成以及基于Docker的容器化技术解决了这一问题，实现了灵活的部署。
“
基于深度学习的预测性维护综述”作者：U. Khan, D. Cheng, F. Setti, F. Fummi, M. Cristani, L. Capogrosso。本文综述了工业4.0和工业5.0时代基于学习的预测性维护策略。鉴于工业数据量的增长以及预测性维护在减少停机时间和延长设备寿命方面的关键作用，本文回顾了主要的学习模型和范式，介绍了数据驱动的流程、实际应用案例、评估指标以及先进的预测性维护硬件。
最后，我们要感谢所有为本期特刊的成功做出贡献的人士。首先感谢作者们提交的高质量论文，同时也感谢审稿人的宝贵反馈，这些反馈显著提升了论文的质量。特别感谢主编Tulika Mitra教授以及特刊编辑Andreas Gerstlauer教授和Hiren Patel教授在整个过程中的支持与指导，还要感谢技术团队的专业协助。感谢大家的付出与支持。
Sara Vinco
意大利都灵理工大学
David Broman
瑞典斯德哥尔摩皇家理工学院
客座编辑
