论文标题
第四次研讨会的会议记录，用于对真实系统进行正式分析的模型
Proceedings of the 4th Workshop on Models for Formal Analysis of Real Systems
论文作者
论文摘要
该卷包含《火星2020年的会议记录》，这是针对欧洲关于软件理论和实践的欧洲联合会议的现实系统正式分析模型的第四次研讨会。 火星研讨会汇集了来自不同社区的研究人员，这些研究人员正在开发正式的实际系统模型，例如发生复杂模型的领域，例如网络，网络物理系统，硬件/软件代码，生物学，等等。 火星讲习班源于两个观察： （1）大型案例研究必须表明规范形式主义和建模技术适用于实际系统，而许多研究论文仅考虑玩具示例或小案例研究。 （2）开发真实系统的准确模型通常需要大量时间，通常是几个月或数年。但是，在大多数科学论文中，由于缺乏空间，需要跳过该模型的显着细节，并为正式验证方法和结果留出空间。 火星研讨会的补救措施是这些问题，强调建模而不是验证，以保留从正式建模中学到的经验教训，这些建模通常不会在其他地方讨论。
This volume contains the proceedings of MARS 2020, the fourth workshop on Models for Formal Analysis of Real Systems held as part of ETAPS 2020, the European Joint Conferences on Theory and Practice of Software. The MARS workshop brings together researchers from different communities who are developing formal models of real systems in areas where complex models occur, such as networks, cyber-physical systems, hardware/software codesign, biology, etc. The MARS workshops stem from two observations: (1) Large case studies are essential to show that specification formalisms and modelling techniques are applicable to real systems, whereas many research papers only consider toy examples or tiny case studies. (2) Developing an accurate model of a real system takes a large amount of time, often months or years. In most scientific 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. The MARS workshop remedies these issues, emphasising modelling over verification, so as to retain lessons learnt from formal modelling, which are not usually discussed elsewhere.
