NDLI: ORIS: a tool for state-space analysis of real-time preemptive systems

Content Provider	IEEE Xplore Digital Library
Author	Bucci, G. Sassoli, L. Vicario, E.
Copyright Year	2004
Description	Author affiliation: Dipt. Sistemi e Informatica, Firenze Univ., Florence, Italy (Bucci, G.; Sassoli, L.; Vicario, E.)
Abstract	Formal methods based on state-space enumeration, such as timed automata and time Petri nets (TPN), have been proposed for designing and validating reactive real-time systems. The great expressiveness of these methods is counterbalanced by the increased complexity of the analysis, which may grow exponentially. Furthermore, the enumerated state-space needs to be inspected to identify critical behaviors with respect to sequencing and timing requirements. This naturally leads to the implementation of tools supporting the different stages of the development process. In this paper we present Oris, an environment for building, simulating, analyzing and validating complex real time systems specified in terms of an extended TPN formalism, named preemptive time Petri nets. Oris includes not only the state-space enumeration engine, but also a number of modules which ease user interaction, and make it usable also by a designer with no specific experience in formal modelling.
Sponsorship	Fac. of Electr. Eng., Math. and Comput. Sci., Univ. of Twente R. Netherlands Acad. of Arts and Sci. Netherlands Organ. for Sci. Res. Centre for Telematics and Inf. Technol., Univ. of Twente Inst. for programming Res. and Algorithmics
Starting Page	70
Ending Page	79
File Size	1176851
Page Count	10
File Format	PDF
ISBN	0769521851
DOI	10.1109/QEST.2004.1348021
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2004-09-27
Publisher Place	The Netherlands
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Real time systems Analytical models Processor scheduling Petri nets Buildings Automata Timing Engines Delay Clocks
Content Type	Text
Resource Type	Article

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

Timed state space analysis of real-time preemptive systems

Modeling flexible real time systems with preemptive time Petri nets

A translation based method for the timed analysis of scheduling extended time Petri nets

Introducing probability within state class analysis of dense-time-dependent systems

Schedulability analysis of real-time systems using timing constraint Petri nets

Analysis of Real Time Systems through the ORIS Tool

Correctness verification and performance analysis of real-time systems using stochastic preemptive time Petri nets

Development of a Schedulability Analysis Framework Based on pTPN and UPPAAL with Stopwatches

On-the-fly TCTL model checking for Time Petri Nets using state class graphs

ORIS: a tool for state-space analysis of real-time preemptive systems

Similar Documents

Timed state space analysis of real-time preemptive systems

Modeling flexible real time systems with preemptive time Petri nets

A translation based method for the timed analysis of scheduling extended time Petri nets

Introducing probability within state class analysis of dense-time-dependent systems

Schedulability analysis of real-time systems using timing constraint Petri nets

Analysis of Real Time Systems through the ORIS Tool

Correctness verification and performance analysis of real-time systems using stochastic preemptive time Petri nets

Development of a Schedulability Analysis Framework Based on pTPN and UPPAAL with Stopwatches

On-the-fly TCTL model checking for Time Petri Nets using state class graphs

ORIS: a tool for state-space analysis of real-time preemptive systems