This volume contains the proceedings of MARS 2024, the sixth workshop on Models for Formal Analysis of Real Systems, held as part of ETAPS 2024, the European Joint Conferences on Theory and Practice of Software. The MARS workshops bring 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 co-design, biology, etc. The motivation and aim for MARS stem from the following 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 workshops aim at remedying these issues, emphasising modelling over verification, so as to retain lessons learnt from formal modelling, which are not usually discussed elsewhere.
翻译:本卷收录了MARS 2024(第六届实际系统形式化分析模型研讨会)的论文集。该研讨会作为ETAPS 2024(欧洲软件理论与应用联合会议)的一部分举办。MARS研讨会汇聚了来自不同领域的研究人员,共同致力于在复杂模型出现的领域(如网络、信息物理系统、硬件/软件协同设计、生物学等)构建实际系统的形式化模型。MARS的动机和目标源于以下两点观察:(1)大型案例研究对于证明规范形式化和建模技术适用于实际系统至关重要,而许多研究论文仅考虑玩具示例或小型案例研究。(2)开发实际系统的精确模型需要大量时间,往往长达数月甚至数年。然而,在大多数科学论文中,由于篇幅限制以及需要为形式化验证方法和结果留出空间,模型的重要细节常被略去。MARS研讨会旨在解决这些问题,强调建模而非验证,以便保留从形式化建模中汲取的经验教训,而这些经验通常在其他场合鲜有讨论。