MCLab Group List of Papers -- Query Results

	MCLab Group List of Papers Home \| Show All \| Simple Search \| Advanced Search	Login Quick Search: Field: contains: ...
	91–100 of 143 records found matching your query (RSS):

Search & Display Options

Select All Deselect All

<< 1 2 3 4 5 6 7 8 9 10 >> [11–15]

List View

Citations

Details

	Records
	Author	Bobbio, Andrea; Ciancamerla, Ester; Minichino, Michele; Tronci, Enrico
	Title	Functional analysis of a telecontrol system and stochastic measures of its GSM/GPRS connections			Type	Journal Article
	Year	2005	Publication	Archives of Transport – International Journal of Transport Problems	Abbreviated Journal
	Volume	17	Issue	3-4	Pages
	Keywords
	Abstract
	Address
	Corporate Author				Thesis
	Publisher		Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ jtp05			Serial	31
Permanent link to this record



	Author	Campagnano, Edoardo; Ciancamerla, Ester; Minichino, Michele; Tronci, Enrico
	Title	Automatic Analysis of a Safety Critical Tele Control System			Type	Conference Article
	Year	2005	Publication	24th International Conference on: Computer Safety, Reliability, and Security (SAFECOMP)	Abbreviated Journal
	Volume		Issue		Pages	94-107
	Keywords
	Abstract	We show how the Mur$\varphi$ model checker can be used to automatically carry out safety analysis of a quite complex hybrid system tele-controlling vehicles traffic inside a safety critical transport infrastructure such as a long bridge or a tunnel. We present the Mur$\varphi$ model we developed towards this end as well as the experimental results we obtained by running the Mur$\varphi$ verifier on our model. Our experimental results show that the approach presented here can be used to verify safety of critical dimensioning parameters (e.g. bandwidth) of the telecommunication network embedded in a safety critical system.
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication	Fredrikstad, Norway	Editor	Winther, R.; Gran, B. A.; Dahll, G.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	3688	Series Issue		Edition
	ISSN	3-540-29200-4	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ safecomp05			Serial	32
Permanent link to this record



	Author	Intrigila, Benedetto; Magazzeni, Daniele; Melatti, Igor; Tronci, Enrico
	Title	A Model Checking Technique for the Verification of Fuzzy Control Systems			Type	Conference Article
	Year	2005	Publication	CIMCA '05: Proceedings of the International Conference on Computational Intelligence for Modelling, Control and Automation and International Conference on Intelligent Agents, Web Technologies and Internet Commerce Vol-1 (CIMCA-IAWTIC'06)	Abbreviated Journal
	Volume		Issue		Pages	536-542
	Keywords
	Abstract	Fuzzy control is well known as a powerful technique for designing and realizing control systems. However, statistical evidence for their correct behavior may be not enough, even when it is based on a large number of samplings. In order to provide a more systematic verification process, the cell-to-cell mapping technology has been used in a number of cases as a verification tool for fuzzy control systems and, more recently, to assess their optimality and robustness. However, cell-to-cell mapping is typically limited in the number of cells it can explore. To overcome this limitation, in this paper we show how model checking techniques may be instead used to verify the correct behavior of a fuzzy control system. To this end, we use a modified version of theMurphi verifier, which ease the modeling phase by allowing to use finite precision real numbers and external C functions. In this way, also already designed simulators may be used for the verification phase. With respect to the cell mapping technique, our approach appears to be complementary; indeed, it explores a much larger number of states, at the cost of being less informative on the global dynamic of the system.
	Address
	Corporate Author				Thesis
	Publisher	IEEE Computer Society	Place of Publication	Washington, DC, USA	Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	0-7695-2504-0-01	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Immt05			Serial	75
Permanent link to this record



	Author	Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico
	Title	Exploiting Hub States in Automatic Verification			Type	Conference Article
	Year	2005	Publication	Automated Technology for Verification and Analysis: Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings	Abbreviated Journal
	Volume		Issue		Pages	54-68
	Keywords
	Abstract	In this paper we present a new algorithm to counteract state explosion when using Explicit State Space Exploration to verify protocol-like systems. We sketch the implementation of our algorithm within the Caching Mur$\varphi$ verifier and give experimental results showing its effectiveness. We show experimentally that, when memory is a scarce resource, our algorithm improves on the time performances of Caching Mur$\varphi$ verification algorithm, saving between 16% and 68% (45% on average) in computation time.
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication		Editor	D.A. Peled; Y.-K. Tsay
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	3707	Series Issue		Edition
	ISSN	3-540-29209-8	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Dimt04			Serial	83
Permanent link to this record



	Author	Gorrieri, Roberto; Lanotte, Ruggero; Maggiolo-Schettini, Andrea; Martinelli, Fabio; Tini, Simone; Tronci, Enrico
	Title	Automated analysis of timed security: a case study on web privacy			Type	Journal Article
	Year	2004	Publication	International Journal of Information Security	Abbreviated Journal
	Volume	2	Issue	3-4	Pages	168-186
	Keywords
	Abstract	This paper presents a case study on an automated analysis of real-time security models. The case study on a web system (originally proposed by Felten and Schneider) is presented that shows a timing attack on the privacy of browser users. Three different approaches are followed: LH-Timed Automata (analyzed using the model checker HyTech), finite-state automata (analyzed using the model checker NuSMV), and process algebras (analyzed using the model checker CWB-NC). A comparative analysis of these three approaches is given.
	Address
	Corporate Author				Thesis
	Publisher		Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ ijis04			Serial	33
Permanent link to this record



	Author	Lanotte, Ruggero; Maggiolo-Schettini, Andrea; Tini, Simone; Troina, Angelo; Tronci, Enrico
	Title	Automatic Covert Channel Analysis of a Multilevel Secure Component			Type	Conference Article
	Year	2004	Publication	Information and Communications Security, 6th International Conference, ICICS 2004, Malaga, Spain, October 27-29, 2004, Proceedings	Abbreviated Journal
	Volume		Issue		Pages	249-261
	Keywords
	Abstract	The NRL Pump protocol defines a multilevel secure component whose goal is to minimize leaks of information from high level systems to lower level systems, without degrading average time performances. We define a probabilistic model for the NRL Pump and show how a probabilistic model checker (FHP-mur$\varphi$) can be used to estimate the capacity of a probabilistic covert channel in the NRL Pump. We are able to compute the probability of a security violation as a function of time for various configurations of the system parameters (e.g. buffer sizes, moving average size, etc). Because of the model complexity, our results cannot be obtained using an analytical approach and, because of the low probabilities involved, it can be hard to obtain them using a simulator.
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication		Editor	Lopez, J.; Qing, S.; Okamoto, E.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	3269	Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ icics04			Serial	34
Permanent link to this record



	Author	Martinelli, Marco; Tronci, Enrico; Dipoppa, Giovanni; Balducelli, Claudio
	Title	Electric Power System Anomaly Detection Using Neural Networks			Type	Conference Article
	Year	2004	Publication	8th International Conference on: Knowledge-Based Intelligent Information and Engineering Systems (KES)	Abbreviated Journal
	Volume		Issue		Pages	1242-1248
	Keywords
	Abstract	The aim of this work is to propose an approach to monitor and protect Electric Power System by learning normal system behaviour at substations level, and raising an alarm signal when an abnormal status is detected; the problem is addressed by the use of autoassociative neural networks, reading substation measures. Experimental results show that, through the proposed approach, neural networks can be used to learn parameters underlaying system behaviour, and their output processed to detecting anomalies due to hijacking of measures, changes in the power network topology (i.e. transmission lines breaking) and unexpected power demand trend.
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication	Wellington, New Zealand	Editor	Negoita, M.G.; Howlett, R.J.; Jain, L.C.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	3213	Series Issue		Edition
	ISSN	3-540-23318-0	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ kes04			Serial	35
Permanent link to this record



	Author	Lanotte, Ruggero; Maggiolo-Schettini, Andrea; Tini, Simone; Troina, Angelo; Tronci, Enrico
	Title	Automatic Analysis of the NRL Pump			Type	Journal Article
	Year	2004	Publication	Electr. Notes Theor. Comput. Sci.	Abbreviated Journal
	Volume	99	Issue		Pages	245-266
	Keywords
	Abstract	We define a probabilistic model for the NRL Pump and using FHP-mur$\varphi$ show experimentally that there exists a probabilistic covert channel whose capacity depends on various NRL Pump parameters (e.g. buffer size, number of samples in the moving average, etc).
	Address
	Corporate Author				Thesis
	Publisher		Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ entcs04			Serial	36
Permanent link to this record



	Author	Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa
	Title	Bounded Probabilistic Model Checking with the Mur$\varphi$ Verifier			Type	Conference Article
	Year	2004	Publication	Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings	Abbreviated Journal
	Volume		Issue		Pages	214-229
	Keywords
	Abstract	In this paper we present an explicit verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. We restrict ourselves to verification of Bounded PCTL formulas (BPCTL), that is, PCTL formulas in which all Until operators are bounded, possibly with different bounds. This means that we consider only paths (system runs) of bounded length. Given a Markov Chain $\cal M$ and a BPCTL formula Φ, our algorithm checks if Φ is satisfied in $\cal M$. This allows to verify important properties, such as reliability in Discrete Time Hybrid Systems. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$) such extension of the Mur$\varphi$ verifier. We give experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can effectively handle verification of BPCTL formulas for systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication		Editor	Hu, A.J.; Martin, A.K.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	3312	Series Issue		Edition
	ISSN	3-540-23738-0	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Dimtz04			Serial	87
Permanent link to this record



	Author	Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa
	Title	Exploiting Transition Locality in Automatic Verification of Finite State Concurrent Systems			Type	Journal Article
	Year	2004	Publication	Sttt	Abbreviated Journal
	Volume	6	Issue	4	Pages	320-341
	Keywords
	Abstract	In this paper we show that statistical properties of the transition graph of a system to be verified can be exploited to improve memory or time performances of verification algorithms. We show experimentally that protocols exhibit transition locality. That is, with respect to levels of a breadth-first state space exploration, state transitions tend to be between states belonging to close levels of the transition graph. We support our claim by measuring transition locality for the set of protocols included in the Mur$\varphi$ verifier distribution. We present a cache-based verification algorithm that exploits transition locality to decrease memory usage and a disk-based verification algorithm that exploits transition locality to decrease disk read accesses, thus reducing the time overhead due to disk usage. Both algorithms have been implemented within the Mur$\varphi$ verifier. Our experimental results show that our cache-based algorithm can typically save more than 40% of memory with an average time penalty of about 50% when using (Mur$\varphi$) bit compression and 100% when using bit compression and hash compaction, whereas our disk-based verification algorithm is typically more than ten times faster than a previously proposed disk-based verification algorithm and, even when using 10% of the memory needed to complete verification, it is only between 40 and 530% (300% on average) slower than (RAM) Mur$\varphi$ with enough memory to complete the verification task at hand. Using just 300 MB of memory our disk-based Mur$\varphi$ was able to complete verification of a protocol with about $10^9$ reachable states. This would require more than 5 GB of memory using standard Mur$\varphi$.
	Address
	Corporate Author				Thesis
	Publisher		Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ DIMTZ04j			Serial	91
Permanent link to this record