arXivDaily arXiv每日学术速递 周一至周五更新
arXiv周末暂无论文更新,休息一下吧,周末愉快~~
arXiv 2604.03053cs.LOcs.SE
收藏

第七届形式分析现实系统模型研讨会论文集

Proceedings of the 7th Workshop on Models for Formal Analysis of Real Systems

Maurice H. ter Beek, Gregor Gössler

AI总结:

本文集旨在通过大规模案例研究展示形式化规范和建模技术在现实系统中的应用,强调建模而非验证,保留形式化建模中的经验教训,为未来分析和比较奠定基础。

摘要:

这些论文集收录了在2026年4月12日于意大利都灵举行的第七届形式分析现实系统模型研讨会(MARS 2026)上发表的论文,作为第29届国际软件理论与实践联合会议(ETAPS 2026)的卫星会议。MARS的目标是将来自不同社区的研究人员聚集在一起,这些社区在复杂模型出现的领域(例如网络、物理系统、硬件/软件协同设计、生物学)中开发形式化模型。MARS的动机源于两个观察:1)大规模案例研究对于展示规范形式化和建模技术在现实系统中的适用性至关重要,而许多论文只考虑玩具示例或小案例研究;2)开发一个准确的现实系统模型需要大量时间,通常为几个月或几年。然而,在大多数论文中,由于空间限制,模型的显著细节需要被跳过,以留出空间给形式化验证方法和结果。MARS旨在解决这些问题,强调建模而非验证,以保留形式化建模中通常在其他地方未讨论的经验教训,这些可能为未来分析和比较奠定基础。

英文摘要:

These proceedings contain the papers that were presented at the 7th Workshop on Models for Formal Analysis of Real Systems (MARS 2026), which took place on 12 April 2026 in Turin, Italy, as a satellite event of the 29th International Joint Conferences on Theory and Practice of Software (ETAPS 2026). The goal of MARS is to bring together researchers from different communities who are developing formal models of real systems in areas where complex models occur (e.g., networks, cyber-physical systems, hardware/software codesign, biology). The motivation for MARS stems from the following two observations: - Large case studies are essential to show that specification formalisms and modelling techniques are applicable to real systems, whereas many papers only consider toy examples or tiny case studies. - Developing an accurate model of a real system takes a large amount of time, often months or years. In most papers, however, salient details of the model need to be skipped due to lack of space, and to leave room for formal verification methodologies and results. MARS aims at remedying these issues, emphasising modelling over verification, so as to retain lessons learned from formal modelling, which are not usually discussed elsewhere, and which may lay the basis for future analysis and comparison.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑