Home | [1–10] << 11 12 13 14 15 >> |
Records | |||||
---|---|---|---|---|---|
Author | Barbanera, Franco; Dezani-Ciancaglini, Mariangiola; Salvo, Ivano; Sassone, Vladimiro | ||||
Title | A Type Inference Algorithm for Secure Ambients | Type | Journal Article | ||
Year | 2002 | Publication | Electronic Notes in Theoretical Computer Science | Abbreviated Journal | |
Volume | 62 | Issue | Pages | 83-101 | |
Keywords | |||||
Abstract | We consider a type discipline for the Ambient Calculus that associates ambients with security levels and constrains them to be traversed by or opened in ambients of higher security clearance only. We present a bottom-up algorithm that, given an untyped process P, computes a minimal set of constraints on security levels such that all actions during runs of P are performed without violating the security level priorities. Such an algorithm appears to be a prerequisite to use type systems to ensure security properties in the web scenario. | ||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | Elsevier | 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 | TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types | Approved | yes | ||
Call Number | Sapienza @ mari @ Barbanera-Dezani-Salvo-Sassone:01 | Serial | 73 | ||
Permanent link to this record | |||||
Author | Melatti, I.; Mari, F.; Mancini, T.; Prodanovic, M.; Tronci, E. | ||||
Title | A Two-Layer Near-Optimal Strategy for Substation Constraint Management via Home Batteries | Type | Journal Article | ||
Year | 2021 | Publication | IEEE Transactions on Industrial Electronics | Abbreviated Journal | |
Volume | Issue | Pages | 1-1 | ||
Keywords | |||||
Abstract | Within electrical distribution networks, substation constraints management requires that aggregated power demand from residential users is kept within suitable bounds. Efficiency of substation constraints management can be measured as the reduction of constraints violations w.r.t. unmanaged demand. Home batteries hold the promise of enabling efficient and user-oblivious substation constraints management. Centralized control of home batteries would achieve optimal efficiency. However, it is hardly acceptable by users, since service providers (e.g., utilities or aggregators) would directly control batteries at user premises. Unfortunately, devising efficient hierarchical control strategies, thus overcoming the above problem, is far from easy. We present a novel two-layer control strategy for home batteries that avoids direct control of home devices by the service provider and at the same time yields near-optimal substation constraints management efficiency. Our simulation results on field data from 62 households in Denmark show that the substation constraints management efficiency achieved with our approach is at least 82% of the one obtained with a theoretical optimal centralized strategy. | ||||
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 | To appear | Approved | no | ||
Call Number | MCLab @ davi @ ref9513535 | Serial | 190 | ||
Permanent link to this record | |||||
Author | Fantechi, Alessandro; Gnesi, Stefania; Mazzanti, Franco; Pugliese, Rosario; Tronci, Enrico | ||||
Title | A Symbolic Model Checker for ACTL | Type | Conference Article | ||
Year | 1998 | Publication | International Workshop on Current Trends in Applied Formal Method (FM-Trends) | Abbreviated Journal | |
Volume | Issue | Pages | 228-242 | ||
Keywords | |||||
Abstract | We present SAM, a symbolic model checker for ACTL, the action-based version of CTL. SAM relies on implicit representations of Labeled Transition Systems (LTSs), the semantic domain for ACTL formulae, and uses symbolic manipulation algorithms. SAM has been realized by translating (networks of) LTSs and, possibly recursive, ACTL formulae into BSP (Boolean Symbolic Programming), a programming language aiming at defining computations on boolean functions, and by using the BSP interpreter to carry out computations (i.e. verifications). | ||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | Springer | Place of Publication | Boppard, Germany | Editor | Hutter, D.; Stephan, W.; Traverso, P.; Ullmann, M. |
Language | Summary Language | Original Title | |||
Series Editor | Series Title | Lecture Notes in Computer Science | Abbreviated Series Title | ||
Series Volume | 1641 | Series Issue | Edition | ||
ISSN | 3-540-66462-9 | ISBN | Medium | ||
Area | Expedition | Conference | |||
Notes | Approved | yes | |||
Call Number | Sapienza @ mari @ fm-trends98 | Serial | 51 | ||
Permanent link to this record | |||||
Author | Tronci, Enrico; Della Penna, Giuseppe; Intrigila, Benedetto; Venturini Zilli, Marisa | ||||
Title | A Probabilistic Approach to Automatic Verification of Concurrent Systems | Type | Conference Article | ||
Year | 2001 | Publication | 8th Asia-Pacific Software Engineering Conference (APSEC) | Abbreviated Journal | |
Volume | Issue | Pages | 317-324 | ||
Keywords | |||||
Abstract | The main barrier to automatic verification of concurrent systems is the huge amount of memory required to complete the verification task (state explosion). In this paper we present a probabilistic algorithm for automatic verification via model checking. Our algorithm trades space with time. In particular, when memory is full because of state explosion our algorithm does not give up verification. Instead it just proceeds at a lower speed and its results will only hold with some arbitrarily small error probability. Our preliminary experimental results show that by using our probabilistic algorithm we can typically save more than 30% of RAM with an average time penalty of about 100% w.r.t. a deterministic state space exploration with enough memory to complete the verification task. This is better than giving up the verification task because of lack of memory. | ||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | IEEE Computer Society | Place of Publication | Macau, China | Editor | |
Language | Summary Language | Original Title | |||
Series Editor | Series Title | Abbreviated Series Title | |||
Series Volume | Series Issue | Edition | |||
ISSN | 0-7695-1408-1 | ISBN | Medium | ||
Area | Expedition | Conference | |||
Notes | Approved | yes | |||
Call Number | Sapienza @ mari @ apsec01 | Serial | 43 | ||
Permanent link to this record | |||||
Author | Mari, Federico; Melatti, Igor; Tronci, Enrico; Finzi, Alberto | ||||
Title | A multi-hop advertising discovery and delivering protocol for multi administrative domain MANET | Type | Journal Article | ||
Year | 2013 | Publication | Mobile Information Systems | Abbreviated Journal | Mobile Information Systems |
Volume | 3 | Issue | 9 | Pages | 261-280 |
Keywords | |||||
Abstract | |||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | IOS Press | Place of Publication | Editor | ||
Language | Summary Language | Original Title | |||
Series Editor | Series Title | Abbreviated Series Title | |||
Series Volume | Series Issue | Edition | |||
ISSN | 1574-017x (Print) 1875-905X (Online) | ISBN | Medium | ||
Area | Expedition | Conference | |||
Notes | Approved | no | |||
Call Number | Sapienza @ melatti @ | Serial | 109 | ||
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 | Driouich, Y.; Parente, M.; Tronci, E. | ||||
Title | A methodology for a complete simulation of Cyber-Physical Energy Systems | Type | Conference Article | ||
Year | 2018 | Publication | EESMS 2018 – Environmental, Energy, and Structural Monitoring Systems, Proceedings | Abbreviated Journal | |
Volume | Issue | Pages | 1-5 | ||
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 | no | |||
Call Number | MCLab @ davi @ Driouich20181 | Serial | 169 | ||
Permanent link to this record | |||||
Author | Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico | ||||
Title | A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software | Type | Report | ||
Year | 2012 | Publication | Abbreviated Journal | ||
Volume | abs/1210.2276 | Issue | Pages | ||
Keywords | |||||
Abstract | Many Control Systems are indeed Software Based Control Systems, i.e. control systems whose controller consists of control software running on a microcontroller device. This motivates investigation on Formal Model Based Design approaches for automatic synthesis of control software.
Available algorithms and tools (e.g., QKS) may require weeks or even months of computation to synthesize control software for large-size systems. This motivates search for parallel algorithms for control software synthesis. In this paper, we present a map-reduce style parallel algorithm for control software synthesis when the controlled system (plant) is modeled as discrete time linear hybrid system. Furthermore we present an MPI-based implementation PQKS of our algorithm. To the best of our knowledge, this is the first parallel approach for control software synthesis. We experimentally show effectiveness of PQKS on two classical control synthesis problems: the inverted pendulum and the multi-input buck DC/DC converter. Experiments show that PQKS efficiency is above 65%. As an example, PQKS requires about 16 hours to complete the synthesis of control software for the pendulum on a cluster with 60 processors, instead of the 25 days needed by the sequential algorithm in QKS. |
||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | CoRR, Technical Report | 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 @ | Serial | 101 | ||
Permanent link to this record | |||||
Author | Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico | ||||
Title | A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software | Type | Conference Article | ||
Year | 2013 | Publication | Proc. of International SPIN Symposium on Model Checking of Software (SPIN 2013) | Abbreviated Journal | International SPIN Symposium on Model Checking of Software |
Volume | Issue | Pages | 43-60 | ||
Keywords | |||||
Abstract | |||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | Springer - Verlag | Place of Publication | Editor | ||
Language | Summary Language | Original Title | |||
Series Editor | Series Title | Lecture Notes in Computer Science | Abbreviated Series Title | ||
Series Volume | 7976 | Series Issue | Edition | ||
ISSN | 0302-9743 | ISBN | 978-3-642-39175-0 | Medium | |
Area | Expedition | Conference | |||
Notes | Approved | no | |||
Call Number | Sapienza @ melatti @ | Serial | 112 | ||
Permanent link to this record | |||||
Author | Alimguzhin, V.; Mari, F.; Melatti, I.; Tronci, E.; Ebeid, E.; Mikkelsen, S.A.; Jacobsen, R.H.; Gruber, J.K.; Hayes, B.; Huerta, F.; Prodanovic, M. | ||||
Title | A Glimpse of SmartHG Project Test-bed and Communication Infrastructure | Type | Conference Article | ||
Year | 2015 | Publication | Digital System Design (DSD), 2015 Euromicro Conference on | Abbreviated Journal | |
Volume | Issue | Pages | 225-232 | ||
Keywords | Batteries; Control systems; Databases; Production; Sensors; Servers; Smart grids; Grid State Estimation; Peak Shaving; Policy Robustness Verification; Price Policy Synthesis | ||||
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 | no | |||
Call Number | Sapienza @ preissler @ Alimguzhin_etal2015 | Serial | 127 | ||
Permanent link to this record |