NDLI: Integrating Formal Veriication Methods of Quantitative Real-time Properties into a Development Environment for Robot Controllers Integrating Formal Veriication Methods of Quantitative Real-time Properties into a Development Environment for Robot Controllers

Please wait, while we are loading the content...

Integrating Formal Veriication Methods of Quantitative Real-time Properties into a Development Environment for Robot Controllers Integrating Formal Veriication Methods of Quantitative Real-time Properties into a Development Environment for Robot Controllers

Content Provider	Semantic Scholar
Author	Jourdan, Muriel
Copyright Year	1995
Abstract	In this paper we describe our experience with a development environment for robot controllers, which provides the user with formal veriication func-tionalities. We study how to augment these functionalities by also allowing formal veriication of quantitative real-time properties. Our approach is based on the timed extension of a synchronous language, named Timed-Argos, and on a symbolic model-checking tool named Kronos for the real-time temporal logic TCTL. We illustrate this approach by a real example taken from the area of autonomous vehicles, which poses some challenges on the applicability of the theory and nally, we discuss some possible solutions. This large-scale real application is also an opportunity to identify new research directions in the area of formal veriication. V eriier des propri et es quantitatives temporelles dans un environnement de d eveloppement d'applications robotique R esum e : Nous d ecrivons dans ce rapport comment int egrer des m ethodes de v eriication formelle de propri et es quantitatives temporelles a un environnement d'aide au d e-veloppement d'applications robotique nomm e ORCCAD. Notre approche est bas ee sur l'utilisation d'une extension temporelle du langage synchrone Argos et d'un ou-til de v eriication symbolique nomm e Kronos. Nous illustrons cette approche sur un exemple r eel de conduite autonome de v ehicules. Cette exp erimentation est pour nous l'occasion de valider une approche formelle et de d ecouvrir de nouveaux besoins aan d'orienter les recherches men ees dans le domaine de la v eriication formelle des syst emes temps-r eels.
File Format	PDF HTM / HTML
Language	English
Access Restriction	Open
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in