检索结果-南通市图书馆

Towards a verified compiler prototype for the synchronous language SIGNAL

Frontiers of Computer Science 2016年第1期10卷 37-53页

作者： Zhibin YANG Jean-Paul BODEVEIX Mamoun FILALI Kai HU Yongwang ZHAO Dianfu MA College of Computer Science and Technology Nanjing University of Aeronautics and Astronautics Nanjing 210016 China IRIT-CNRS Universite de Toulouse Toulouse 31062 France State Key Laboratory of Software Development Environment Beihang University Beijing 100191 China

SIGNAL belongs to the synchronous languages family which are widely used in the design of safety-critical real-time systems such as avionics, space systems, and nu- clear power plants. This paper reports a compiler prototype for SIGNAL. Compared with the existing SIGNAL com- piler, we propose a new intermediate representation （named S-CGA, a variant of clocked guarded actions）, to integrate more synchronous programs into our compiler prototype in the future. The front-end of the compiler, i.e., the transla- tion from SIGNAL to S-CGA, is presented. As well, the proof of semantics preservation is mechanized in the theo- rem prover Coq. Moreover, we present the back-end of the compiler, including sequential code generation and multi- threaded code generation with time-predictable properties. With the rising importance of multi-core processors in safety- critical embedded systems or cyber-physical systems （CPS）, there is a growing need for model-driven generation of multi- threaded code and thus mapping on multi-core. We propose a time-predictable multi-core architecture model in archi- tecture analysis and design language （AADL）, and map the multi-threaded code to this model.

关键词： synchronous languages SIGNAL guarded ac-tions verified compiler Coq architecture analysis and designlanguage (AADL)

来源：

维普期刊数据库

同方期刊数据库评论

在线全文

学校读者我要写书评

暂无评论

On the use of formal methods to model and verify neuronal archetypes

引用

Frontiers of Computer Science 2022年第3期16卷 101-122页

作者： Elisabetta DE MARIA Abdorrahim BAHRAMI Thibaud L'YVONNET Amy FELTY Daniel GAFFÉ Annie RESSOUCHE Franck GRAMMONT UniversitéCôte d'zur CNRSI3S06903 Sophia Antipolis CedexFrance School of Electrical Engineering and Computer Science University of OttawaOntarioK1N 6N5Canada UniversitéCôte d'Azur INRIA SAM06902 Sophia Antipolis CedexFrance UniversitéCôte d'Azur CNRSLEAT06903 Sophia Antipolis CedexFrance UniversitéCôte d'Azur CNRSLJAD06108 Nice Cedex 02France

Having a formal model of neural networks can greatly help in understanding and verifying their properties,behavior,and response to external factors such as disease and *** this paper,we adopt a formal model to represent neurons,some neuronal graphs,and their *** specific neuronal graphs are known for having biologically relevant structures and behaviors and we call them *** archetypes are supposed to be the basis of typical instances of neuronal information *** this paper we study six fundamental archetypes(simple series,series with multiple outputs,parallel composition,negative loop,inhibition of a behavior,and contralateral inhibition),and we consider two ways to couple two archetypes:(i)connecting the output(s)of the first archetype to the input(s)of the second archetype and(ii)nesting the first archetype within the second *** report and compare two key approaches to the formal modeling and verification of the proposed neuronal archetypes and some selected *** first approach exploits the synchronous programming language Lustre to encode archetypes and their couplings,and to express properties concerning their dynamic *** properties are verified thanks to the use of model *** second approach relies on a theorem prover,the Coq Proof Assistant,to prove dynamic properties of neurons and archetypes.

关键词： neuronal networks leaky integrate and fire modeling synchronous languages model checking theorem proving Lustre Coq formal methods

来源：

维普期刊数据库

同方期刊数据库评论

在线全文

学校读者我要写书评

暂无评论

欢迎您,

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

在线全文

在线全文

请选择保存的检索档案：

请选择收藏分类：

通借通还

欢迎您,

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

在线全文

在线全文

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：