形式语言与自动机学术速递[12.24]
Update！H5支持摘要折叠，体验更佳！点击阅读原文访问arxivdaily.com，涵盖CS|物理|数学|经济|统计|金融|生物|电气领域，更有搜索、收藏等功能！
cs.FL形式语言与自动机，共计2篇
【1】 A Manifesto for Applicable Formal Methods
标题：关于适用的形式化方法的一个宣言
链接：https://arxiv.org/abs/2112.12758
摘要：Formal methods were frequently shown to be effective and, perhaps because of
that, practitioners are interested in using them more often. Still, these
methods are far less applied than expected, particularly, in critical domains
where they are strongly recommended and where they have the greatest potential.
Our hypothesis is that formal methods still seem not to be applicable enough or
ready for their intended use. In critical software engineering, what do we mean
when we speak of a formal method? And what does it mean for such a method to be
applicable both from a scientific and practical viewpoint? Based on what the
literature tells about the first question, with this manifesto, we lay out a
set of principles that when followed by a formal method give rise to its mature
applicability in a given scope. Rather than exercising criticism of past
developments, this manifesto strives to foster an increased use of formal
methods to the maximum benefit.
【2】 Safety assurance of an industrial robotic control system using hardware/software co-verification
标题：基于软硬件协同验证的工业机器人控制系统安全性保证
链接：https://arxiv.org/abs/2112.12248
机构：Dept. of Mechatronics, University of Agder (UiA), Norway, Dept. of Computer Science, University of York, UK, Robotics Group, Norwegian University of Life Sciences (NMBU), Norway, ABB Robotics, Bryne, Norway
摘要：As a general trend in industrial robotics, an increasing number of safety
functions are being developed or re-engineered to be handled in software rather
than by physical hardware such as safety relays or interlock circuits. This
trend reinforces the importance of supplementing traditional, input-based
testing and quality procedures which are widely used in industry today, with
formal verification and model-checking methods. To this end, this paper focuses
on a representative safety-critical system in an ABB industrial paint robot,
namely the High-Voltage electrostatic Control system (HVC). The practical
convergence of the high-voltage produced by the HVC, essential for safe
operation, is formally verified using a novel and general co-verification
framework where hardware and software models are related via platform mappings.
This approach enables the pragmatic combination of highly diverse and
specialised tools. The paper's main contribution includes details on how
hardware abstraction and verification results can be transferred between tools
in order to verify system-level safety properties. It is noteworthy that the
HVC application considered in this paper has a rather generic form of a
feedback controller. Hence, the co-verification framework and experiences
reported here are also highly relevant for any cyber-physical system tracking a
setpoint reference.
机器翻译，仅供参考
点击“阅读原文”获取带摘要的学术速递