Publications

book

  1. Villafiorita, A. (2014). Introduction to Software Project Management. Auerbach Publications. [Link] @book{Villafiorita:2014aa, author = {Villafiorita, Adolfo}, title = {Introduction to Software Project Management}, publisher = {Auerbach Publications}, year = {2014}, month = mar, pub_type = {book}, category = {spm}, link = {http://www.spmbook.com}, month_numeric = {3} }

  2. Bozzano, M., & Villafiorita, A. (2010). Design and Safety Assessment of Critical Systems - A formal methods perspective. CRC Press (Taylor and Francis). [Link] [Abstract] Safety-critical systems - namely systems whose failure may cause death or injury to people, harm to the environment, or economical loss - are becoming more complex, both in the type of functionality they provide and in the way they are demanded to interact with the environment. Traditionally, safety analysis techniques and procedures are used to identify risks and hazards, with the goal of eliminating, avoiding, or reducing the probability of failure. However, these techniques are often performed manually, hence they are a time-consuming activity itself vulnerable to human error, since they rely on the ability of the safety engineer to understand and to foresee system behavior. The growing complexity of safety-critical systems requires an adequate increase in the capability of safety engineers to assess system safety, encouraging the adoption of formal techniques. This book is an introduction to the area of design and verification of safety critical systems, with a focus on safety assessment using formal methods. After an introduction covering the fundamental concepts in the areas of safety and reliability, the book illustrates the issues related to the design, development, and safety assessment of critical systems. The core of the book covers some of the most well-known notations, techniques, and procedures, and explains in detail how formal methods can be used to realize such procedures. Traditional verification and validation techniques and new trends in formal methods for safety assessment are described. The books ends with a discussion on the role of formal methods in the certification process. The book provides an in-depth and hands-on view on the application of formal techniques, that are applicable to a variety of industrial sectors, such as transportation, avionics and aerospace, and nuclear power. @book{Bozzano:2010ly, author = {Bozzano, Marco and Villafiorita, Adolfo}, title = {Design and Safety Assessment of Critical Systems - A formal methods perspective}, publisher = {CRC Press (Taylor and Francis)}, year = {2010}, abstract = {Safety-critical systems - namely systems whose failure may cause death or injury to people, harm to the environment, or economical loss - are becoming more complex, both in the type of functionality they provide and in the way they are demanded to interact with the environment. Traditionally, safety analysis techniques and procedures are used to identify risks and hazards, with the goal of eliminating, avoiding, or reducing the probability of failure. However, these techniques are often performed manually, hence they are a time-consuming activity itself vulnerable to human error, since they rely on the ability of the safety engineer to understand and to foresee system behavior. The growing complexity of safety-critical systems requires an adequate increase in the capability of safety engineers to assess system safety, encouraging the adoption of formal techniques. This book is an introduction to the area of design and verification of safety critical systems, with a focus on safety assessment using formal methods. After an introduction covering the fundamental concepts in the areas of safety and reliability, the book illustrates the issues related to the design, development, and safety assessment of critical systems. The core of the book covers some of the most well-known notations, techniques, and procedures, and explains in detail how formal methods can be used to realize such procedures. Traditional verification and validation techniques and new trends in formal methods for safety assessment are described. The books ends with a discussion on the role of formal methods in the certification process. The book provides an in-depth and hands-on view on the application of formal techniques, that are applicable to a variety of industrial sectors, such as transportation, avionics and aerospace, and nuclear power.}, pub_type = {book}, category = {safety_analysis}, link = {http://www.safety-critical.org} }

editor

  1. Costa, P., Ferlan, C., & Villafiorita, A. (Eds.). (2013). Chi Porta da Mangiare? Il Cibo tra eccessi e scarsit{`a}. FBK Press. [Link] @book{:2013aa, editor = {Costa, Paolo and Ferlan, Claudio and Villafiorita, Adolfo}, title = {Chi Porta da Mangiare? Il Cibo tra eccessi e scarsit{`a}}, category = {food}, publisher = {FBK Press}, year = {2013}, month = dec, pub_type = {editor}, link = {https://books.fbk.eu/pubblicazioni/titoli/chi-porta-da-mangiare-il-cibo-tra-eccessi-e-scarsita/}, month_numeric = {12} }

  2. Popescu-Zeletin, R., Jonas, K., Rai, I. A., Glitho, R., & Villafiorita, A. (Eds.). (2012). E-Infrastructures and E-Services on Developing Countries: Third International ICST Conference, AFRICOMM 2011, Zanzibar, Tanzania, November 23-24 (Vol. 92). Springer. [Link] [Abstract] This book constitutes the thoroughly refereed post-conference proceedings of the Third International ICST Conference on e-Infrastructure and e-Services for Developing Countries, AFRICOMM 2011, held in Zanzibar, Tansania, in November 2011. The 24 revised full papers presented together with 2 poster papers were carefully reviewed and selected from numerous submissions. The papers cover a wide range of topics in the field of information and communication infrastructures. They are organized in two tracks: communication infrastructures for developing countries and electronic services, ICT policy, and regulatory issues for developing countries. @proceedings{africomm-2011, title = {E-Infrastructures and E-Services on Developing Countries: Third International ICST Conference, AFRICOMM 2011, Zanzibar, Tanzania, November 23-24}, year = {2012}, editor = {Popescu-Zeletin, Radu and Jonas, Karl and Rai, Idris A. and Glitho, R. and Villafiorita, Adolfo}, volume = {92}, month = apr, organization = {LNICST}, publisher = {Springer}, abstract = {This book constitutes the thoroughly refereed post-conference proceedings of the Third International ICST Conference on e-Infrastructure and e-Services for Developing Countries, AFRICOMM 2011, held in Zanzibar, Tansania, in November 2011. The 24 revised full papers presented together with 2 poster papers were carefully reviewed and selected from numerous submissions. The papers cover a wide range of topics in the field of information and communication infrastructures. They are organized in two tracks: communication infrastructures for developing countries and electronic services, ICT policy, and regulatory issues for developing countries.}, pub_type = {editor}, category = {ict4d}, link = {http://www.springer.com/computer/general+issues/book/978-3-642-29092-3}, month_numeric = {4} }

  3. Popescu-Zeletin, R., Rai, I. A., Jonas, K., & Villafiorita, A. (Eds.). (2011). E-Infrastructures and E-Services on Developing Countries: Second International ICST Conference, AFRICOMM 2010, Cape Town, South Africa. Springer. [Link] @proceedings{africomm-2010, title = {E-Infrastructures and E-Services on Developing Countries: Second International ICST Conference, AFRICOMM 2010, Cape Town, South Africa}, year = {2011}, editor = {Popescu-Zeletin, Radu and Rai, Idris A. and Jonas, Karl and Villafiorita, Adolfo}, month = oct, organization = {LNICST}, publisher = {Springer}, pub_type = {editor}, category = {ict4d}, link = {http://www.springer.com/computer/general+issues/book/978-3-642-23827-7?cm_mmc=event-_-bookAuthor-_-congratulation-_-0&cm_mmc=EVENT-_-BookAuthorEmail-_-}, month_numeric = {10} }

  4. Villafiorita, A., Regis, S.-P., & Zorer, A. (Eds.). (2010). E-Infrastructures and E-Services on Developing Countries: First International ICST Conference, AFRICOMM December 2009, Maputo, Mozambique (Vol. 38). Springer. [Link] @proceedings{africomm-2009, title = {E-Infrastructures and E-Services on Developing Countries: First International ICST Conference, AFRICOMM December 2009, Maputo, Mozambique}, year = {2010}, editor = {Villafiorita, Adolfo and Regis, Saint-Paul and Zorer, Alessandro}, volume = {38}, month = jun, organization = {LNICST}, publisher = {Springer}, pub_type = {editor}, category = {ict4d}, link = {http://www.springer.com/978-3-642-12700-7}, month_numeric = {6} }

book_chapter

  1. Al-Shammari, A. F. N., & Villafiorita, A. (2014). {A Synthesis of Vote Verification Methods in Electronic Voting Systems}. In Design, Development, and Use of Secure Electronic Voting Systems. IGI Global. [Link] @incollection{Al-Shammari2014A, author = {Al-Shammari, Ali Fawzi Najm and Villafiorita, Adolfo}, title = {{A Synthesis of Vote Verification Methods in Electronic Voting Systems}}, booktitle = {Design, Development, and Use of Secure Electronic Voting Systems}, publisher = {IGI Global}, year = {2014}, pub_type = {book_chapter}, link = {http://www.igi-global.com/book/design-development-use-secure-electronic/94868}, category = {evoting} }

  2. Villafiorita, A. (2013). Spreco Alimentare e nuove Tecnologie. In Chi Porta da Mangiare? Il Cibo tra eccessi e scarsit{`a}. FBK Press. @incollection{Villafiorita:2013aa, author = {Villafiorita, Adolfo}, title = {Spreco Alimentare e nuove Tecnologie}, booktitle = {Chi Porta da Mangiare? Il Cibo tra eccessi e scarsit{`a}}, publisher = {FBK Press}, year = {2013}, category = {food}, pub_type = {book_chapter} }

  3. Weldemariam, K., & Villafiorita, A. (2012). Analyzing the Security of Electronic Voting Systems: Can Formal Methods Really Help? In M. Gupta, J. Walp, & R. Sharman (Eds.), Threats, Countermeasures, and Advances in Applied Information Security (pp. 361–380). IGI. @incollection{WelVil12, author = {Weldemariam, Komminist and Villafiorita, Adolfo}, title = {Analyzing the Security of Electronic Voting Systems: Can Formal Methods Really Help?}, booktitle = {Threats, Countermeasures, and Advances in Applied Information Security}, publisher = {IGI}, year = {2012}, editor = {Gupta, M. and Walp, J. and Sharman, R.}, pages = {361-380}, pub_type = {book_chapter}, category = {evoting} }

  4. Bozzano, M., & Villafiorita, A. (2012). Safety Critical Systems. In Encyclopedia of Software Engineering. CRC Press, Taylor \& Francis Group. [Abstract] Safety critical systems—namely systems on which human lives depend—have to remain functional not only in nominal conditions, that is, when everything works as expected, but also when some of their components do not behave as expected. The methodologies, activities, and techniques to tackle this engineering challenge go under the name of safety analysis. This entry is an introduction to the development of safety critical systems with emphasis on some emerging techniques to support automated analysis and verification of complex systems. @incollection{BozVil12, author = {Bozzano, Marco and Villafiorita, Adolfo}, title = {Safety Critical Systems}, booktitle = {Encyclopedia of Software Engineering}, publisher = {CRC Press, Taylor \& Francis Group}, year = {2012}, abstract = {Safety critical systems—namely systems on which human lives depend—have to remain functional not only in nominal conditions, that is, when everything works as expected, but also when some of their components do not behave as expected. The methodologies, activities, and techniques to tackle this engineering challenge go under the name of safety analysis. This entry is an introduction to the development of safety critical systems with emphasis on some emerging techniques to support automated analysis and verification of complex systems.}, pub_type = {book_chapter}, category = {safety_analysis} }

  5. Ciaghi, A., & Villafiorita, A. (2012). Law Modeling and {BPR} for {Public Administration Improvement}. In Handbook of Research on E-Government in Emerging Economies: Adoption, E-Participation, and Legal Frameworks (pp. 391–410). IGI. [Download] [Abstract] ICTs are becoming more present in Public Administrations and in legal knowledge management. In most countries it is now possible for citizens to freely access the text of acts, bills, judgments, etc. Analysts that work on re-engineering Public Administration processes must take into account all relevant sources of law as they will ultimately be modified in order to legitimize the new processes. In this chapter, we consider the requirements to design a framework for Business Process Re-Engineering for Public Administrations by analyzing the existing systems for legal knowledge representation and interchange and the current technologies to assist modeling and change management of Business Processes. The ultimate goal is that of supporting the law-making process, facilitating the participation of people without a jurisprudence background to the editing of regulations, by providing effective means to comprehend the law, make changes to the law and keep track of the dependencies between the text and the models. @incollection{Ciaghi:2011kx, author = {Ciaghi, Aaron and Villafiorita, Adolfo}, title = {Law Modeling and {BPR} for {Public Administration Improvement}}, booktitle = {Handbook of Research on E-Government in Emerging Economies: Adoption, E-Participation, and Legal Frameworks}, publisher = {IGI}, year = {2012}, pages = {391-410}, month = mar, abstract = {ICTs are becoming more present in Public Administrations and in legal knowledge management. In most countries it is now possible for citizens to freely access the text of acts, bills, judgments, etc. Analysts that work on re-engineering Public Administration processes must take into account all relevant sources of law as they will ultimately be modified in order to legitimize the new processes. In this chapter, we consider the requirements to design a framework for Business Process Re-Engineering for Public Administrations by analyzing the existing systems for legal knowledge representation and interchange and the current technologies to assist modeling and change management of Business Processes. The ultimate goal is that of supporting the law-making process, facilitating the participation of people without a jurisprudence background to the editing of regulations, by providing effective means to comprehend the law, make changes to the law and keep track of the dependencies between the text and the models.}, pub_type = {book_chapter}, category = {ict4laws}, link = {http://ict4g.net/adolfo/downloads/papers/law_modeling_and_bpr-2012.pdf}, month_numeric = {3} }

  6. Weldemariam, K., & Villafiorita, A. (2012). Analyzing the Security of Electronic Voting Systems: Can Formal Methods Really Help? In M. Gupta, J. Walp, & R. Sharman (Eds.), Strategic and Practical Approaches for Information Security Governance: Technologies and Applied Solutions. IGI. [Link] [Abstract] In this chapter, first we discuss the current trends in the usage of formal techniques in the development of e-voting system. We then present our experiences on their usage to specify and verify the behaviors of one of currently deployed e-voting systems using formal techniques and verification against a subset of critical security properties that the system should meet. We also specified attacks that have been shown to successfully compromise the system. The attack information is used to extend the original specification of the system and derive what we called the extended model. This work is a step towards fostering open specification and the (partial) verification of a voting machine. The specification and verification was intended as a learning process where we would use formal techniques to improve the current development of e-voting systems. @incollection{Weldemariam:2011fk, author = {Weldemariam, Komminist and Villafiorita, Adolfo}, title = {Analyzing the Security of Electronic Voting Systems: Can Formal Methods Really Help?}, booktitle = {Strategic and Practical Approaches for Information Security Governance: Technologies and Applied Solutions}, publisher = {IGI}, year = {2012}, editor = {Gupta, Manish and Walp, John and Sharman, Raj}, month = feb, abstract = {In this chapter, first we discuss the current trends in the usage of formal techniques in the development of e-voting system. We then present our experiences on their usage to specify and verify the behaviors of one of currently deployed e-voting systems using formal techniques and verification against a subset of critical security properties that the system should meet. We also specified attacks that have been shown to successfully compromise the system. The attack information is used to extend the original specification of the system and derive what we called the extended model. This work is a step towards fostering open specification and the (partial) verification of a voting machine. The specification and verification was intended as a learning process where we would use formal techniques to improve the current development of e-voting systems. }, pub_type = {book_chapter}, category = {evoting}, link = {http://www.igi-global.com/book/strategic-practical-approaches-information-security/58283}, month_numeric = {2} }

  7. Cernuzzi, L., Gonzalez, M., Ronchetti, M., Villafiorita, A., & Weldemariam, K. (2011). Multi-cultural experiences in eGovernance: Case Studies and a Roadmap. In W. C. Danilo Piagessi Kristian Sund (Ed.), Global Strategy and Practice of e-Governance: Examples from Around the World. IGI. [Link] [Abstract] In a world characterized by rapid change driven by globalization, an ICT-based economy transformation poses some challenges and opportunities for the private sector and the government sector alike. ICT has for some time been at the core of government tasks, inseparable from strategy, planning, consultation and implementation to improve citizen’s life in different ways. Nevertheless, indications are that the government sector has been falling behind in these practices (mostly in developing countries), compared to the private sector. This realization has prompted some governments to put ICT high on their policy agendas, with the aim of introducing ICT-based solutions to improve their public administration processes, and thus deliver «quality public services». We define ICT for Good (ICT4G) as the use of ICT to addressing critical problems in societies characterized by low ICT penetration in a way that life is impacted for the better. Along this line, we have been working on the design, development, and evaluation of ICT solutions that directly require the involvement of citizen on the usage of the developed system itself and/or on the decision-making processes. In this chapter, we discuss our experiences and lessons learned in this holistic approach to e-Governance projects from the ICT4G perspective and the role it can play for developing countries. @incollection{Cernuzzi:2010ve, author = {Cernuzzi, Luca and Gonzalez, Magal'{i} and Ronchetti, Marco and Villafiorita, Adolfo and Weldemariam, Komminist}, title = {Multi-cultural experiences in eGovernance: Case Studies and a Roadmap}, booktitle = {Global Strategy and Practice of e-Governance: Examples from Around the World}, publisher = {IGI}, year = {2011}, editor = {Danilo Piagessi, Kristian Sund, Walter Castelnovo}, abstract = {In a world characterized by rapid change driven by globalization, an ICT-based economy transformation poses some challenges and opportunities for the private sector and the government sector alike. ICT has for some time been at the core of government tasks, inseparable from strategy, planning, consultation and implementation to improve citizen’s life in different ways. Nevertheless, indications are that the government sector has been falling behind in these practices (mostly in developing countries), compared to the private sector. This realization has prompted some governments to put ICT high on their policy agendas, with the aim of introducing ICT-based solutions to improve their public administration processes, and thus deliver «quality public services». We define ICT for Good (ICT4G) as the use of ICT to addressing critical problems in societies characterized by low ICT penetration in a way that life is impacted for the better. Along this line, we have been working on the design, development, and evaluation of ICT solutions that directly require the involvement of citizen on the usage of the developed system itself and/or on the decision-making processes. In this chapter, we discuss our experiences and lessons learned in this holistic approach to e-Governance projects from the ICT4G perspective and the role it can play for developing countries.}, pub_type = {book_chapter}, category = {egov4dev_countries}, link = {http://www.igi-global.com/book/global-strategy-practice-governance/46168} }

  8. Shvaiko, P., Villafiorita, A., Zorer, A., Chemane, L., & Fumo, T. (2010). {eGovernment Interoperability Framework}: a case Study in a Developing Country. In C. G. Reddick (Ed.), Comparative E-Government (1st ed., Vol. 25). Springer. [Link] [Abstract] Harmonizing decentralized development of ICT solutions with centralized strategies, e.g., meant to favor reuse and optimization of resources, is a complex technical and organizational challenge. The problem, shared by virtually all the governments, is becoming a priority also for countries, such as Mozambique, that have started their ICT policy relatively recently and for which it is now evident that — if no particular attention is devoted to the interoperability of the solutions being developed — the result will rapidly become a patchwork of solutions incompatible with each other. The focus of the paper is on formulation of eGIF4M: eGovernment Interoperability Framework for Mozambique. The framework is based on a holistic approach. It builds on top of the existing experiences in eGIFs all over the world and it addresses some specific needs and peculiarities of developing countries, like Mozambique. The result is a comprehensive framework based on: (i) a reference architecture along with technical standards, (ii) a standardization life cycle, (iii) a maturity model, and (iv) some key actions meant to make the initiative sustainable in the longer term. @incollection{Shvaiko:2010zr, author = {Shvaiko, Pavel and Villafiorita, Adolfo and Zorer, Alessandro and Chemane, Lourino and Fumo, Teot{'o}nio}, title = {{eGovernment Interoperability Framework}: a case Study in a Developing Country}, booktitle = {Comparative E-Government}, publisher = {Springer}, year = {2010}, editor = {Reddick, Christopher G}, volume = {25}, series = {Integrated Series in Information Systems}, edition = {1st}, abstract = {Harmonizing decentralized development of ICT solutions with centralized strategies, e.g., meant to favor reuse and optimization of resources, is a complex technical and organizational challenge. The problem, shared by virtually all the governments, is becoming a priority also for countries, such as Mozambique, that have started their ICT policy relatively recently and for which it is now evident that — if no particular attention is devoted to the interoperability of the solutions being developed — the result will rapidly become a patchwork of solutions incompatible with each other. The focus of the paper is on formulation of eGIF4M: eGovernment Interoperability Framework for Mozambique. The framework is based on a holistic approach. It builds on top of the existing experiences in eGIFs all over the world and it addresses some specific needs and peculiarities of developing countries, like Mozambique. The result is a comprehensive framework based on: (i) a reference architecture along with technical standards, (ii) a standardization life cycle, (iii) a maturity model, and (iv) some key actions meant to make the initiative sustainable in the longer term.}, isbn = {978-1-4419-6535-6}, pub_type = {book_chapter}, tags = {egif4m-2010.pdf}, category = {egov4dev_countries}, link = {http://www.springer.com/it/book/9781441965356} }

journal

  1. Grau, I., Travassos, G. H., Cernuzzi, L., & Villafiorita, A. (2015). Tape Mbo’e: A First Experimental Assessment. CLEI Electronic Journal, 18, CIbSE 2014 Special Issue(1), 26. [Link] [Abstract] The development of software not only needs to consider the construction process, but also other aspects such as cost, human resources and communication among stakeholders. The lack of simplicity into this context becomes explicit when some restrictions, such as service oriented architecture, must be considered as the basic style to build sustainable applications into environments were practitioners are not aware of this software technology. In addition to this, most of the available software processes are not directly applicable nor are they reusable, so learning times becomes risk for the development of the project. Therefore, Tape Mbo´e (TME) has been proposed to support the building of such applications, into development environments like developing countries where we can have economic constraints and scarcity of proficient practitioners. The first application of TME has been to develop a service-based application whose goal is to provide the interoperability among legacy systems of different public agencies in Paraguay. Initial results of this experience indicated the feasibility and simplicity of TME when applied in this field. The evaluation process, its results and conclusions are described in this paper. @article{Grau:2015aa, author = {Grau, Ilse and Travassos, Guilherme H. and Cernuzzi, Luca and Villafiorita, Adolfo}, title = {Tape Mbo’e: A First Experimental Assessment}, journal = {CLEI electronic journal}, year = {2015}, volume = {18, CIbSE 2014 Special Issue}, number = {1}, pages = {26}, month = apr, abstract = {The development of software not only needs to consider the construction process, but also other aspects such as cost, human resources and communication among stakeholders. The lack of simplicity into this context becomes explicit when some restrictions, such as service oriented architecture, must be considered as the basic style to build sustainable applications into environments were practitioners are not aware of this software technology. In addition to this, most of the available software processes are not directly applicable nor are they reusable, so learning times becomes risk for the development of the project. Therefore, Tape Mbo´e (TME) has been proposed to support the building of such applications, into development environments like developing countries where we can have economic constraints and scarcity of proficient practitioners. The first application of TME has been to develop a service-based application whose goal is to provide the interoperability among legacy systems of different public agencies in Paraguay. Initial results of this experience indicated the feasibility and simplicity of TME when applied in this field. The evaluation process, its results and conclusions are described in this paper. }, pub_type = {journal}, link = {http://www.clei.org/cleiej/paper.php?id=328}, category = {egov4dev_countries}, month_numeric = {4} }

  2. Weldemariam, K., Kemmerer, R. A., & Villafiorita, A. (2011). Formal analysis of an electronic voting system: An experience report. Journal of Systems and Software, 84(10), 1618–1637. [Abstract] We have seen that several currently deployed e-voting systems share critical failures in their design and implementation that render their technical and procedural controls insufficient to guarantee trustworthy voting. The application of formal methods would greatly help to better address problems associated with assurance against requirements and standards. More specifically, it would help to thoroughly specify and analyze the underlying assumptions and security specific properties, and it would improve the trustworthiness of the final systems. In this article, we show how such techniques can be used to model and reason about the security of one of the currently deployed e-voting systems in the U.S.A named ES&S. We used the ASTRAL language to specify the voting process of ES&S machines and the critical security requirements for the system. Proof obligations that verify that the specified system meets the critical requirements were automatically generated by the ASTRAL Software Development Environment (SDE). The PVS interactive theorem prover was then used to apply the appropriate proof strategies and discharge the proof obligations. We also believe that besides analyzing the system against its requirements, it is equally important to perform an analysis under malicious circumstances where the execution model is augmented with attack behaviors. Thus, we extend the formal specification of the system by specifying attacks that have been shown to successfully compromise the system, and we then repeat the formal verification. This is helpful in detecting missing requirements or unwarranted assumptions about the specification of the system. In addition, this allows one to sketch countermeasure strategies to be used when the system behaves differently than it should and to build confidence about the system under development. Finally, we acknowledge the main problem that arises in e-voting system specification and verification: modeling attacks is very difficult because the different types of attack often cut across the structure of the original behavior models, thus making (incremental or compositional) verification very difficult. @article{Weldemariam20111618, author = {Weldemariam, Komminist and Kemmerer, Richard A. and Villafiorita, Adolfo}, title = {Formal analysis of an electronic voting system: An experience report}, journal = {Journal of Systems and Software}, year = {2011}, volume = {84}, number = {10}, pages = {1618-1637}, abstract = {We have seen that several currently deployed e-voting systems share critical failures in their design and implementation that render their technical and procedural controls insufficient to guarantee trustworthy voting. The application of formal methods would greatly help to better address problems associated with assurance against requirements and standards. More specifically, it would help to thoroughly specify and analyze the underlying assumptions and security specific properties, and it would improve the trustworthiness of the final systems. In this article, we show how such techniques can be used to model and reason about the security of one of the currently deployed e-voting systems in the U.S.A named ES&S. We used the ASTRAL language to specify the voting process of ES&S machines and the critical security requirements for the system. Proof obligations that verify that the specified system meets the critical requirements were automatically generated by the ASTRAL Software Development Environment (SDE). The PVS interactive theorem prover was then used to apply the appropriate proof strategies and discharge the proof obligations. We also believe that besides analyzing the system against its requirements, it is equally important to perform an analysis under malicious circumstances where the execution model is augmented with attack behaviors. Thus, we extend the formal specification of the system by specifying attacks that have been shown to successfully compromise the system, and we then repeat the formal verification. This is helpful in detecting missing requirements or unwarranted assumptions about the specification of the system. In addition, this allows one to sketch countermeasure strategies to be used when the system behaves differently than it should and to build confidence about the system under development. Finally, we acknowledge the main problem that arises in e-voting system specification and verification: modeling attacks is very difficult because the different types of attack often cut across the structure of the original behavior models, thus making (incremental or compositional) verification very difficult.}, pub_type = {journal}, category = {evoting} }

  3. Weldemariam, K., & Villafiorita, A. (2011). Procedural Security Analysis: A Methodological Approach. Journal of Systems and Software, 84(7), 1114–1129. https://doi.org/10.1016/j.jss.2011.01.064 [Link] [Abstract] This article introduces what we call procedural security analysis, an approach that allows for a systematic security assessment of (business) processes. The approach is based on explicit reasoning on asset flows and is implemented by building formal models to describe the nominal procedures under analysis, by injecting possible threat-actions of such models, and by assuming that any combination of threats can be possible in all steps into such models. We use the NuSMV input language to encode the asset flows, which are amenable for formal analysis. This allows us to understand how the switch to a new techno- logical solution changes the requirements of an organization, with the ultimate goal of defining the new processes that ensure a sufficient level of security. We have applied the technique to a real-world electronic voting system named ProVotE to analyze the procedures used during and after elections. Such analyses are essential to identify the limits of the current procedures (i.e., conditions under which attacks are undetectable) and to identify the hypotheses that can guarantee reasonably secure electronic elections. Additionally, the results of the analyses can be a step forward to devise a set of requirements, to be applied both at the organizational level and on the (software) systems to make them more secure. @article{Weldemariam:2011yq, author = {Weldemariam, Komminist and Villafiorita, Adolfo}, title = {Procedural Security Analysis: A Methodological Approach}, journal = {Journal of Systems and Software}, year = {2011}, volume = {84}, number = {7}, pages = {1114-1129}, month = jul, abstract = {This article introduces what we call procedural security analysis, an approach that allows for a systematic security assessment of (business) processes. The approach is based on explicit reasoning on asset flows and is implemented by building formal models to describe the nominal procedures under analysis, by injecting possible threat-actions of such models, and by assuming that any combination of threats can be possible in all steps into such models. We use the NuSMV input language to encode the asset flows, which are amenable for formal analysis. This allows us to understand how the switch to a new techno- logical solution changes the requirements of an organization, with the ultimate goal of defining the new processes that ensure a sufficient level of security. We have applied the technique to a real-world electronic voting system named ProVotE to analyze the procedures used during and after elections. Such analyses are essential to identify the limits of the current procedures (i.e., conditions under which attacks are undetectable) and to identify the hypotheses that can guarantee reasonably secure electronic elections. Additionally, the results of the analyses can be a step forward to devise a set of requirements, to be applied both at the organizational level and on the (software) systems to make them more secure.}, doi = {10.1016/j.jss.2011.01.064}, pub_type = {journal}, category = {evoting}, link = {http://authors.elsevier.com/TrackPaper.html?trk_article=JSS8661&trk_surname=Weldemariam}, month_numeric = {7} }

  4. Weldemariam, K., Siena, A., Villafiorita, A., & Susi, A. (2011). {Enhancing Law Modeling and Analysis: using {BPR}-Based and Goal-Oriented Frameworks}. International Journal on Advances in Security, 3(3-4), 80–90. [Link] [Abstract] In recent years, new laws have been enacted to explicitly regulate sensitive matters such as business and health assistance, when, for example, performed on networked systems. Existing laws have been revised and also gained new meaning when referred to an Internet-based activity. As a result of this, concerns like security, privacy and governance are increasingly the focus of (digital) government regulations around the world. This trend has created a challenge in the definition and/or redesign of Public Administration (PA) processes. This trend has also created a challenge in the compliance of regulations, whereby PA officers, lawmakers, software engineers are required to ensure that their software delivery complies with relevant regulations, either through design or reengineering activity. Previously we proposed two complementary frameworks — the Nomos and VLPM frameworks — to systematically model and analyze laws. Nomos is a goal-oriented approach to effectively capture high-level principles in terms of goal realization for the requirements guided by the satisfiability of normative proposition(s) obtained from rules embedded in the law. VLPM, whereas is a tool-supported BPR methodology to extract laws represented in XML and build models using a subset of UML diagrams. In this paper1, we provide detailed overview of the two frameworks and their integration whose aim is to improve the current modeling and analysis of laws by providing a uniform environment that can be used both at modeling time and for laws assessment. The integration of process and goal-oriented ontologies with the VLPM framework would also make easier the modeling and analysis of laws and procedures and provide a facility for interchanging models among the tools. We believe that, this provides a framework that allows tracing and reasoning either top-down, from the principles to the implementation or, vice versa, bottom-up, from a change in the procedure to the principles. It is exactly this connection that adds value to the solution we propose and makes our approach more significant than the simple juxtaposition of the two techniques. Finally, we use an example to examine the combined offer. @article{Weldemariam:2011kx, author = {Weldemariam, Komminist and Siena, Alberto and Villafiorita, Adolfo and Susi, Angelo}, title = {{Enhancing Law Modeling and Analysis: using {BPR}-Based and Goal-Oriented Frameworks}}, journal = {International Journal on Advances in Security}, year = {2011}, volume = {3}, number = {3-4}, pages = {80-90}, month = apr, abstract = {In recent years, new laws have been enacted to explicitly regulate sensitive matters such as business and health assistance, when, for example, performed on networked systems. Existing laws have been revised and also gained new meaning when referred to an Internet-based activity. As a result of this, concerns like security, privacy and governance are increasingly the focus of (digital) government regulations around the world. This trend has created a challenge in the definition and/or redesign of Public Administration (PA) processes. This trend has also created a challenge in the compliance of regulations, whereby PA officers, lawmakers, software engineers are required to ensure that their software delivery complies with relevant regulations, either through design or reengineering activity. Previously we proposed two complementary frameworks — the Nomos and VLPM frameworks — to systematically model and analyze laws. Nomos is a goal-oriented approach to effectively capture high-level principles in terms of goal realization for the requirements guided by the satisfiability of normative proposition(s) obtained from rules embedded in the law. VLPM, whereas is a tool-supported BPR methodology to extract laws represented in XML and build models using a subset of UML diagrams. In this paper1, we provide detailed overview of the two frameworks and their integration whose aim is to improve the current modeling and analysis of laws by providing a uniform environment that can be used both at modeling time and for laws assessment. The integration of process and goal-oriented ontologies with the VLPM framework would also make easier the modeling and analysis of laws and procedures and provide a facility for interchanging models among the tools. We believe that, this provides a framework that allows tracing and reasoning either top-down, from the principles to the implementation or, vice versa, bottom-up, from a change in the procedure to the principles. It is exactly this connection that adds value to the solution we propose and makes our approach more significant than the simple juxtaposition of the two techniques. Finally, we use an example to examine the combined offer.}, pub_type = {journal}, category = {ict4laws}, link = {http://www.iariajournals.org/security/tocv3n34.html}, month_numeric = {4} }

  5. Bryl, V., Dalpiaz, F., Ferrario, R., Mattioli, A., & Villafiorita, A. (2009). Evaluating procedural alternatives: a case study in e-voting. Electronic Government, an International Journal, 6(2), 213–231. [Abstract] This paper describes part of the work within the ProVotE project, whose goal is the introduction of e-voting systems for local elections. The approach is aimed at providing both precise models of the electoral processes and mechanisms for documenting and reasoning on the possible alternative implementations of the procedures. It is based on defining an alternating sequence of models, written using UML and Tropos. The UML is used to represent electoral processes (both existing and future), while Tropos provides a mean to reason and document the decisions taken about how to change the existing procedures to support an electronic election. @article{Bryl:2009ys, author = {Bryl, Volha and Dalpiaz, Fabiano and Ferrario, Roberta and Mattioli, Andrea and Villafiorita, Adolfo}, title = {Evaluating procedural alternatives: a case study in e-voting}, journal = {Electronic Government, an International Journal}, year = {2009}, volume = {6}, number = {2}, pages = {213 - 231}, abstract = {This paper describes part of the work within the ProVotE project, whose goal is the introduction of e-voting systems for local elections. The approach is aimed at providing both precise models of the electoral processes and mechanisms for documenting and reasoning on the possible alternative implementations of the procedures. It is based on defining an alternating sequence of models, written using UML and Tropos. The UML is used to represent electoral processes (both existing and future), while Tropos provides a mean to reason and document the decisions taken about how to change the existing procedures to support an electronic election.}, pub_type = {journal}, category = {evoting} }

  6. Villafiorita, A., Weldemariam, K., & Tiella, R. (2009). Development, Formal Verification, and Evaluation of an E-Voting System With {VVPAT}. IEEE Transactions on Information Forensics and Security, 4(4 part 1), 651–661. [Abstract] The use of new technologies to support voting has been and is the subject of great debate. Several people advocate the benefits it can bring — such as improved speed and accuracy in counting, accessibility, voting from home — and as many are concerned with the risks it poses, such as unequal access (digital divide), violation to secrecy and anonymity, alteration of the results of an election (because of malicious attacks, bad design/coding, or procedural weaknesses). The attitude of different governments towards electronic voting (e-voting) varies accordingly. In this paper we present the activities related to the development and formal verification of an e-voting system, called ProVotE . ProVotE is an end-to-end e-voting system with Voter Verified Paper Audit Trial (VVPAT), developed within the framework of a larger initiative whose goal is assessing the feasibility of introducing e-voting in the Autonomous Province of Trento. ProVotE has been used in trials and elections with legal value in Italy. What we believe to be of interest is the approach we took for its development, which has been based on a participatory design for the definition of the voter interface, on the usage of formal methods and model checking for the validation of the core logic of the machine, on open source components, and on the formal analysis of some critical procedures related to the usage of the machine during the election. @article{Villafiorita:2009vn, author = {Villafiorita, Adolfo and Weldemariam, Komminist and Tiella, Roberto}, title = {Development, Formal Verification, and Evaluation of an E-Voting System With {VVPAT}}, journal = {IEEE Transactions on Information Forensics and Security}, year = {2009}, volume = {4}, number = {4 part 1}, pages = {651-661}, month = dec, abstract = {The use of new technologies to support voting has been and is the subject of great debate. Several people advocate the benefits it can bring — such as improved speed and accuracy in counting, accessibility, voting from home — and as many are concerned with the risks it poses, such as unequal access (digital divide), violation to secrecy and anonymity, alteration of the results of an election (because of malicious attacks, bad design/coding, or procedural weaknesses). The attitude of different governments towards electronic voting (e-voting) varies accordingly. In this paper we present the activities related to the development and formal verification of an e-voting system, called ProVotE . ProVotE is an end-to-end e-voting system with Voter Verified Paper Audit Trial (VVPAT), developed within the framework of a larger initiative whose goal is assessing the feasibility of introducing e-voting in the Autonomous Province of Trento. ProVotE has been used in trials and elections with legal value in Italy. What we believe to be of interest is the approach we took for its development, which has been based on a participatory design for the definition of the voter interface, on the usage of formal methods and model checking for the validation of the core logic of the machine, on open source components, and on the formal analysis of some critical procedures related to the usage of the machine during the election.}, pub_type = {journal}, category = {evoting}, month_numeric = {12} }

  7. Bozzano, M., & Villafiorita, A. (2007). The {FSAP/NuSMV-SA} Safety Analysis Platform. International Journal on Software Tools for Technology Transfer, 9(1), 5–24. [Abstract] Safety-critical systems are becoming more com- plex, both in the type of functionality they provide and in the way they are demanded to interact with the environment. Such growing complexity requires an adequate increase in the capability of safety engineers to assess system safety, in- cluding analyzing the behaviour of a system in degraded sit- uations. Formal verification techniques, like symbolic model checking, have the potential of dealing with such a complex- ity and are now being used more often. However, existing techniques have little tool support and therefore their use for safety analysis remains limited. In this paper we present FSAP/NuSMV-SA, a platform which aims to improve the development cycle of complex systems by providing a uniform environment that can be used both at design time and for safety assessment. The platform makes the modeling and safety assessment of complex sys- tems easier by providing a facility for automatically augment- ing a system model with failure modes, whose definitions are retrieved from a predefined library. In this way, it is possible to assess the system safety both in nominal conditions and in user-specified degraded situations, that is, in the presence of faults. Furthermore, the platform provides a pattern-based definition of temporal logic formulas, which simplifies the definition of safety requirements. The platform consists of a graphical user interface (FSAP) and an engine (NuSMV-SA) which is based on the NuSMV model checker. The model checking engine provides support for system simulation and standard model checking capabilities, like property verification and the generation of counterexamples. Furthermore, algorithms have been imple- mented to automate the generation of artifacts that are typi- cal of reliability analysis, for example fault trees. The plat- form can derive fault trees automatically (for both monotonic and non-monotonic systems) from the definition of the sys- tem model and of the possible faults. The interface of the platform has been designed to im- prove usability for people that are not expert in formal verifi- cation. The platform has been evaluated in collaboration with an industrial partner and tested on some industrial case studies. @article{Bozzano:2007oz, author = {Bozzano, Marco and Villafiorita, Adolfo}, title = {The {FSAP/NuSMV-SA} Safety Analysis Platform}, journal = {International Journal on Software Tools for Technology Transfer}, year = {2007}, volume = {9}, number = {1}, pages = {5–24}, abstract = {Safety-critical systems are becoming more com- plex, both in the type of functionality they provide and in the way they are demanded to interact with the environment. Such growing complexity requires an adequate increase in the capability of safety engineers to assess system safety, in- cluding analyzing the behaviour of a system in degraded sit- uations. Formal verification techniques, like symbolic model checking, have the potential of dealing with such a complex- ity and are now being used more often. However, existing techniques have little tool support and therefore their use for safety analysis remains limited. In this paper we present FSAP/NuSMV-SA, a platform which aims to improve the development cycle of complex systems by providing a uniform environment that can be used both at design time and for safety assessment. The platform makes the modeling and safety assessment of complex sys- tems easier by providing a facility for automatically augment- ing a system model with failure modes, whose definitions are retrieved from a predefined library. In this way, it is possible to assess the system safety both in nominal conditions and in user-specified degraded situations, that is, in the presence of faults. Furthermore, the platform provides a pattern-based definition of temporal logic formulas, which simplifies the definition of safety requirements. The platform consists of a graphical user interface (FSAP) and an engine (NuSMV-SA) which is based on the NuSMV model checker. The model checking engine provides support for system simulation and standard model checking capabilities, like property verification and the generation of counterexamples. Furthermore, algorithms have been imple- mented to automate the generation of artifacts that are typi- cal of reliability analysis, for example fault trees. The plat- form can derive fault trees automatically (for both monotonic and non-monotonic systems) from the definition of the sys- tem model and of the possible faults. The interface of the platform has been designed to im- prove usability for people that are not expert in formal verifi- cation. The platform has been evaluated in collaboration with an industrial partner and tested on some industrial case studies.}, pub_type = {journal}, publisher = {Springer}, category = {safety_analysis} }

  8. Bundy, A., Giunchiglia, F., Villafiorita, A., & Walsh, T. (1997). Abstract Proof Checking: An Example Motivated by an Incompleteness Theorem. Journal of Automated Reasoning, 19(3), 319–346. [Abstract] We demonstrate the use of abstraction in aiding the construction of an interesting and difficult example in a proof checking system. This experiment demonstrates that abstraction can make proofs easier to comprehend and to verify mechanically. To support such proof checking, we have developed a formal theory of abstraction and added facilities for using abstraction to the GETFOL proof checking system. @article{Bundy:1997pt, author = {Bundy, Alan and Giunchiglia, Fausto and Villafiorita, Adolfo and Walsh, Toby}, title = {Abstract Proof Checking: An Example Motivated by an Incompleteness Theorem}, journal = {Journal of Automated Reasoning}, year = {1997}, volume = {19}, number = {3}, pages = {319–346}, abstract = {We demonstrate the use of abstraction in aiding the construction of an interesting and difficult example in a proof checking system. This experiment demonstrates that abstraction can make proofs easier to comprehend and to verify mechanically. To support such proof checking, we have developed a formal theory of abstraction and added facilities for using abstraction to the GETFOL proof checking system.}, issn = {1573-0670}, pub_type = {journal}, publisher = {Springer}, category = {theorem_proving} }

  9. Giunchiglia, F., Villafiorita, A., & Walsh, T. (1999). Theories of Abstraction. Ai Communications, 10(3-4), 167–176. [Abstract] In the past years, several different theories and frameworks for describing and using abstraction have been proposed. In this paper we overview several of the theories proposed in the past and we argue that each of these works is trying to capture the same intuitive idea, that is, that abstraction is the mapping from one representation of a problem to another which preserves certain desirable properties and which reduces complexity. @article{Giunchiglia:1999xq, author = {Giunchiglia, Fausto and Villafiorita, Adolfo and Walsh, Toby}, title = {Theories of Abstraction}, journal = {Ai Communications}, year = {1999}, volume = {10}, number = {3-4}, pages = {167–176}, abstract = {In the past years, several different theories and frameworks for describing and using abstraction have been proposed. In this paper we overview several of the theories proposed in the past and we argue that each of these works is trying to capture the same intuitive idea, that is, that abstraction is the mapping from one representation of a problem to another which preserves certain desirable properties and which reduces complexity.}, issn = {0921-7126}, pub_type = {journal}, publisher = {IOS Press}, category = {theorem_proving} }

  10. Benerecetti, M., & Villafiorita, A. (1999). Formal specification of Beliefs in Multi-Agents Systems. International Journal of Intelligent Systems, 14(10), 1021–1040. [Abstract] The goal of this paper is to present a logical framework for the formalization of agents’ mutual beliefs in a Multi Agent system. The approach is based on a combination of exten- sional specifications of beliefs and context-based (finite) presentation of the specifications by employing a particular class of Multi Context systems. The extensional specification provides a set-theoretic characterization of beliefs in terms of sets closed under certain conditions. Its finite presentation is provided by using as constructors inference rules in- side a Multi Context system. The resulting framework allows for capturing many relevant cases of real (non omniscient) agents, which are very common in Multi Agent scenarios embedded in real world environments. In order to substantiate this claim, two Multi Agent scenarios are formally specified in detail in the specification framework. @article{Benerecetti:1999qq, author = {Benerecetti, Massimo and Villafiorita, Adolfo}, title = {Formal specification of Beliefs in Multi-Agents Systems}, journal = {International Journal of Intelligent Systems}, year = {1999}, volume = {14}, number = {10}, pages = {1021–1040}, note = {10.1002-int.20364.}, abstract = {The goal of this paper is to present a logical framework for the formalization of agents’ mutual beliefs in a Multi Agent system. The approach is based on a combination of exten- sional specifications of beliefs and context-based (finite) presentation of the specifications by employing a particular class of Multi Context systems. The extensional specification provides a set-theoretic characterization of beliefs in terms of sets closed under certain conditions. Its finite presentation is provided by using as constructors inference rules in- side a Multi Context system. The resulting framework allows for capturing many relevant cases of real (non omniscient) agents, which are very common in Multi Agent scenarios embedded in real world environments. In order to substantiate this claim, two Multi Agent scenarios are formally specified in detail in the specification framework.}, pub_type = {journal}, publisher = {Wiley}, category = {theorem_proving} }

  11. Ciaghi, A., Mattioli, A., & Villafiorita, A. (2010). A Tool Supported Methodology for {BPR} in Public Administrations. International Journal of Electronic Governance (IJEG), 3(2). [Link] [Abstract] In Public Administration (PA), business process redesign is an essential activity for reducing costs, has strict connections with laws and is carried out by actors with different backgrounds. This work proposes an approach where changes in the law are mapped in process diagrams in order to highlight and review the impact on processes. This allows for a stricter collaboration among the different people usually involved in Business Process Reengineering (BPR). The methodology takes advantage of the UML notation and is supported by a tool, Visual Law Process Modeller (VLPM), which helps to keep traceability between processes and laws. Finally, we discuss an example in which the methodology was applied to model the transition from electoral processes to e-electoral process. @article{Ciaghi:2010kn, author = {Ciaghi, Aaron and Mattioli, Andrea and Villafiorita, Adolfo}, title = {A Tool Supported Methodology for {BPR} in Public Administrations}, journal = {International Journal of Electronic Governance (IJEG)}, year = {2010}, volume = {3}, number = {2}, abstract = {In Public Administration (PA), business process redesign is an essential activity for reducing costs, has strict connections with laws and is carried out by actors with different backgrounds. This work proposes an approach where changes in the law are mapped in process diagrams in order to highlight and review the impact on processes. This allows for a stricter collaboration among the different people usually involved in Business Process Reengineering (BPR). The methodology takes advantage of the UML notation and is supported by a tool, Visual Law Process Modeller (VLPM), which helps to keep traceability between processes and laws. Finally, we discuss an example in which the methodology was applied to model the transition from electoral processes to e-electoral process.}, pub_type = {journal}, publisher = {InderScience Publishers}, category = {ict4laws}, link = {http://www.inderscience.com/info/inarticle.php?artid=24443} }

conference

  1. Ciaghi, A., Dalvit, L., Gumbo, S., Gunzo, F., Terzoli, A., & Villafiorita, A. (2015). LRIT4AE: Bridging South African and European Competences for Living Labs. In Proceedings of 19th International Education Association of South Africa (IEASA) conference. Port Elizabeth, South Africa. @inproceedings{Ciaghi:2015kn, author = {Ciaghi, Aaron and Dalvit, Lorenzo and Gumbo, Sibukele and Gunzo, Fortunate and Terzoli, Alfredo and Villafiorita, Adolfo}, title = {LRIT4AE: Bridging South African and European Competences for Living Labs}, booktitle = {Proceedings of 19th International Education Association of South Africa (IEASA) conference}, year = {2015}, month = aug, address = {Port Elizabeth, South Africa}, pub_type = {conference}, category = {ict4d}, month_numeric = {8} }

  2. Ciaghi, A., & Villafiorita, A. (2016). Beyond food sharing: Supporting food waste reduction with ICTs. In 2016 IEEE International Smart Cities Conference (ISC2) (pp. 1–6). https://doi.org/10.1109/ISC2.2016.7580874 [Abstract] Guaranteeing food security is key in improving the quality of life of citizens at all levels of society. The recent economic crisis has increased the number of people living in conditions of food poverty, especially in developed regions. Consequently, the reduction of food waste has become an international trending topic. Despite a growing awareness of the importance of reducing waste and managing food surplus, the role of ICTs in this domain is still unclear and rarely documented. In this paper, we describe our almost 5-year experience in developing and experimenting ICT tools to recover food surplus at different stages of the supply chain and we outline the way forward for an integrated set of ICT tools to reduce waste from producers to households. @inproceedings{7580874, author = {Ciaghi, A. and Villafiorita, A.}, title = {Beyond food sharing: Supporting food waste reduction with ICTs}, booktitle = {2016 IEEE International Smart Cities Conference (ISC2)}, year = {2016}, pages = {1-6}, category = {food}, month = sep, pub_type = {conference}, doi = {10.1109/ISC2.2016.7580874}, abstract = {Guaranteeing food security is key in improving the quality of life of citizens at all levels of society. The recent economic crisis has increased the number of people living in conditions of food poverty, especially in developed regions. Consequently, the reduction of food waste has become an international trending topic. Despite a growing awareness of the importance of reducing waste and managing food surplus, the role of ICTs in this domain is still unclear and rarely documented. In this paper, we describe our almost 5-year experience in developing and experimenting ICT tools to recover food surplus at different stages of the supply chain and we outline the way forward for an integrated set of ICT tools to reduce waste from producers to households.}, month_numeric = {9} }

  3. Fadhil, A., Matteotti, C., Armellin, G., Villafiorita, A., & Betti, D. (2016). CoachMe: a platform for promoting healthy lifestyle. In F. Patern{`{o}}, K. V{"{a}}{"{a}}n{"{a}}nen, K. Church, J. H{"{a}}kkil{"{a}}, A. Kr{"{u}}ger, & M. Serrano (Eds.), Proceedings of the 18th International Conference on Human-Computer Interaction with Mobile Devices and Services Adjunct, MobileHCI 2016, Florence, Italy, September 6-9, 2016 (pp. 1077–1080). {ACM}. https://doi.org/10.1145/2957265.2965004 [Link] @inproceedings{DBLP:conf/mhci/FadhilMAVB16, author = {Fadhil, Ahmed and Matteotti, Cristina and Armellin, Giampaolo and Villafiorita, Adolfo and Betti, Dario}, title = {CoachMe: a platform for promoting healthy lifestyle}, booktitle = {Proceedings of the 18th International Conference on Human-Computer Interaction with Mobile Devices and Services Adjunct, MobileHCI 2016, Florence, Italy, September 6-9, 2016}, year = {2016}, pages = {1077–1080}, crossref = {DBLP:conf/mhci/2016a}, link = {http://doi.acm.org/10.1145/2957265.2965004}, doi = {10.1145/2957265.2965004}, timestamp = {Thu, 22 Sep 2016 15:39:59 +0200}, bibsource = {dblp computer science bibliography, http://dblp.org}, category = {health}, pub_type = {conference} }

  4. Ciaghi, A., Chatikobo, T., Dalvit, L., Indrajith, D., Mfundiso Miya, P. B. M., & Villafiorita, A. (2016). Hacking for Southern Africa: Collaborative Development of Hyperlocal Services for Marginalised Communities. In P. Cunningham & M. Cunningham (Eds.), IST-Africa 2016 Conference Proceedings. IIMC International Information Management Corporation. [Abstract] This paper describes a collaborative experience in the initial development of hyperlocal services for marginalised communities in Southern Africa. Problems specific to urban, peri-urban and rural contexts were identified in collaboration with local community members and NGOs in South Africa and Angola. Selected topics were presented to a group of volunteer developers for initial proof-of-concept application development at an event hosted in Italy. The volunteers produced 6 prototype applications that were demonstrated at the end of the event to a panel of experts and members of one of the interested rural communities. @inproceedings{ciaghi16:_hackin_south_afric, author = {Ciaghi, Aaron and Chatikobo, Tatenda and Dalvit, Lorenzo and Indrajith, Darsha and Mfundiso Miya, Pietro Benedetto Molini and Villafiorita, Adolfo}, title = {Hacking for Southern Africa: Collaborative Development of Hyperlocal Services for Marginalised Communities}, booktitle = {IST-Africa 2016 Conference Proceedings}, year = {2016}, editor = {Cunningham, Paul and Cunningham, Miriam}, month = may, organization = {IIMC International Information Management Corporation}, isbn = {978-1-905824-54-0}, abstract = {This paper describes a collaborative experience in the initial development of hyperlocal services for marginalised communities in Southern Africa. Problems specific to urban, peri-urban and rural contexts were identified in collaboration with local community members and NGOs in South Africa and Angola. Selected topics were presented to a group of volunteer developers for initial proof-of-concept application development at an event hosted in Italy. The volunteers produced 6 prototype applications that were demonstrated at the end of the event to a panel of experts and members of one of the interested rural communities.}, pub_type = {conference}, category = {ict4d}, month_numeric = {5} }

  5. Grau, I., Cernuzzi, L., & Villafiorita, A. (2014). Analyzing Service Oriented Methodologies for Sustainable Applications. XXXII International Conference of The Chilean Computer Science Society. @proceedings{Grau:2014aa, title = {Analyzing Service Oriented Methodologies for Sustainable Applications}, year = {2014}, booktitle = {XXXII International Conference of The Chilean Computer Science Society}, author = {Grau, Ilse and Cernuzzi, Luca and Villafiorita, Adolfo}, pub_type = {conference}, category = {egov4dev_countries} }

  6. Al-Shammari, A. F. N., & Villafiorita, A. (2014). Iraqi Elections in 2014: a Privacy Requirement Evaluation Based on a Polling Place Experience. In Proceeding of INFORMATIK 2014, Big Data-Komplexitat meistern, Stuttgart, Germany (pp. 1359–1370). @inproceedings{Al-Shammari2014, author = {Al-Shammari, Ali Fawzi Najm and Villafiorita, Adolfo}, title = {Iraqi Elections in 2014: a Privacy Requirement Evaluation Based on a Polling Place Experience}, booktitle = {Proceeding of INFORMATIK 2014, Big Data-Komplexitat meistern, Stuttgart, Germany}, year = {2014}, pages = {1359-1370}, pub_type = {conference}, category = {evoting} }

  7. Ciaghi, A., Molini, P., Villafiorita, A., & Weldemariam, K. S. (2013). Maputo living lab summer school of ICTs: An experience report. In IST-Africa Conference and Exhibition (IST-Africa), 2013 (pp. 1–8). [Abstract] This paper presents our experience with the organization of the Summer School of ICTs (SSICT) of Maputo Living Lab. SSICT is a free 1-month course for 3rd and 4th year undergraduate students that provides practical training on the management, design and development of software projects that can have an impact on the local society. The School has been organized for 2 editions in 2011 and 2012 in Maputo, Mozambique and it is part of the larger Maputo Living Lab project. @inproceedings{6701783, author = {Ciaghi, A. and Molini, P. and Villafiorita, A. and Weldemariam, K.S.}, title = {Maputo living lab summer school of ICTs: An experience report}, booktitle = {IST-Africa Conference and Exhibition (IST-Africa), 2013}, year = {2013}, pages = {1-8}, month = may, abstract = {This paper presents our experience with the organization of the Summer School of ICTs (SSICT) of Maputo Living Lab. SSICT is a free 1-month course for 3rd and 4th year undergraduate students that provides practical training on the management, design and development of software projects that can have an impact on the local society. The School has been organized for 2 editions in 2011 and 2012 in Maputo, Mozambique and it is part of the larger Maputo Living Lab project.}, pub_type = {conference}, category = {ict4d}, month_numeric = {5} }

  8. 37th Annual IEEE Computer Software and Applications Conference, COMPSAC 2013, Kyoto, Japan, July 22-26, 2013. (2013). COMPSAC. IEEE Computer Society. @proceedings{DBLP:conf/compsac/2013, title = {37th Annual IEEE Computer Software and Applications Conference, COMPSAC 2013, Kyoto, Japan, July 22-26, 2013}, year = {2013}, booktitle = {COMPSAC}, publisher = {IEEE Computer Society}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6605717}, isbn = {978-0-7695-4986-6}, pub_type = {conference} }

  9. Zewge, A., Weldemariam, K., Hailemariam, S., Villafiorita, A., Susi, A., & Belachew, M. (2012). On the use of goal-oriented methodology for designing agriculture services in developing countries. In Proceedings of the International Conference on Management of Emergent Digital EcoSystems (pp. 40–47). New York, NY, USA: ACM. https://doi.org/10.1145/2457276.2457285 [Link] @inproceedings{Zewge:2012:UGM:2457276.2457285, author = {Zewge, Amanuel and Weldemariam, Komminist and Hailemariam, Sebsibe and Villafiorita, Adolfo and Susi, Angelo and Belachew, Mesfin}, title = {On the use of goal-oriented methodology for designing agriculture services in developing countries}, booktitle = {Proceedings of the International Conference on Management of Emergent Digital EcoSystems}, year = {2012}, series = {MEDES ‘12}, pages = {40–47}, address = {New York, NY, USA}, category = {ict4d}, publisher = {ACM}, acmid = {2457285}, doi = {10.1145/2457276.2457285}, isbn = {978-1-4503-1755-9}, pub_type = {conference}, location = {Addis Ababa, Ethiopia}, numpages = {8}, link = {http://dl.acm.org/citation.cfm?doid=2457276.2457285} }

  10. Al-Shammari, A. F. N., Villafiorita, A., & Weldemariam, K. (2012). Towards an Open Standard Vote Verification Framework in Electronic Voting Systems. In ARES (pp. 437–444). IEEE Computer Society. @inproceedings{DBLP:conf/IEEEares/Al-ShammariVW12a, author = {Al-Shammari, Ali Fawzi Najm and Villafiorita, Adolfo and Weldemariam, Komminist}, title = {Towards an Open Standard Vote Verification Framework in Electronic Voting Systems}, booktitle = {ARES}, year = {2012}, pages = {437-444}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/IEEEares/2012}, ee = {http://doi.ieeecomputersociety.org/10.1109/ARES.2012.42}, category = {evoting}, pub_type = {conference} }

  11. Al-Shammari, A. F. N., Villafiorita, A., & Weldemariam, K. (2012). Understanding the Development Trends of Electronic Voting Systems. In ARES (pp. 186–195). IEEE Computer Society. @inproceedings{DBLP:conf/IEEEares/Al-ShammariVW12, author = {Al-Shammari, Ali Fawzi Najm and Villafiorita, Adolfo and Weldemariam, Komminist}, title = {Understanding the Development Trends of Electronic Voting Systems}, booktitle = {ARES}, year = {2012}, pages = {186-195}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/IEEEares/2012}, ee = {http://doi.ieeecomputersociety.org/10.1109/ARES.2012.76}, category = {evoting}, pub_type = {conference} }

  12. Eshete, B., Villafiorita, A., & Weldemariam, K. (2012). {BINSPECT}: Holistic Analysis and Detection of Malicious Web Pages. In A. D. Keromytis & R. D. Pietro (Eds.), SecureComm (Vol. 106, pp. 149–166). Springer. @inproceedings{DBLP:conf/securecomm/EsheteVW12, author = {Eshete, Birhanu and Villafiorita, Adolfo and Weldemariam, Komminist}, title = {{BINSPECT}: Holistic Analysis and Detection of Malicious Web Pages}, booktitle = {SecureComm}, year = {2012}, pages = {149-166}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/securecomm/2012}, ee = {http://dx.doi.org/10.1007/978-3-642-36883-7_10}, category = {web_development}, pub_type = {conference} }

  13. Eshete, B., Weldemariam, K., Villafiorita, A., & Zulkernine, M. (2013). Confeagle: Automated Analysis of Security Configuration Vulnerabilities in Web Applications. In In Proceedings of the International Conference on Security and Reliability (SERE). @inproceedings{Eshete:2013aa, author = {Eshete, Birhanu and Weldemariam, Komminist and Villafiorita, Adolfo and Zulkernine, Mohammad}, title = {Confeagle: Automated Analysis of Security Configuration Vulnerabilities in Web Applications}, booktitle = {In Proceedings of the International Conference on Security and Reliability (SERE)}, year = {2013}, category = {web_development}, pub_type = {conference} }

  14. Ciaghi, A., Molini, P., Villafiorita, A., & Weldemariam, K. (2013). {M}aputo {L}iving {L}ab {S}ummer {S}chool of {ICT}s: an Experience Report. In Accepted at IST-Africa 2013. @inproceedings{Ciaghi:2013aa, author = {Ciaghi, Aaron and Molini, Pietro and Villafiorita, Adolfo and Weldemariam, Komminist}, title = {{M}aputo {L}iving {L}ab {S}ummer {S}chool of {ICT}s: an Experience Report}, booktitle = {Accepted at IST-Africa 2013}, year = {2013}, category = {ict4d}, pub_type = {conference} }

  15. Ciaghi, A., Eshete, B., Molini, P., & Villafiorita, A. (2013). {SAMo}: Experimenting a Social Accountability Web Platform. In B. Thies & A. Nanavati (Eds.), ACM DEV (p. 17). ACM. @inproceedings{DBLP:conf/dev/CiaghiEMV13, author = {Ciaghi, Aaron and Eshete, Birhanu and Molini, Pietro and Villafiorita, Adolfo}, title = {{SAMo}: Experimenting a Social Accountability Web Platform}, booktitle = {ACM DEV}, year = {2013}, pages = {17}, bibsource = {DBLP, http://dblp.uni-trier.de}, category = {ict4d}, crossref = {DBLP:conf/dev/2013}, ee = {http://doi.acm.org/10.1145/2442882.2442905}, pub_type = {conference} }

  16. Sahilu, H., Belachew, M., Villafiorita, A., Weldemariam, K., & Zewge, A. (2012). Towards Designing an Architecture for Delivering Distributed Agricultural Information Services for Developing Countries. In In International Conference on ICT for Africa 2012, Kampala, Uganda, March 21-24, 2012. @inproceedings{SahBelVil1203, author = {Sahilu, Henok and Belachew, Mesfin and Villafiorita, Adolfo and Weldemariam, Komminist and Zewge, Amanuel}, title = {Towards Designing an Architecture for Delivering Distributed Agricultural Information Services for Developing Countries}, booktitle = {In International Conference on ICT for Africa 2012, Kampala, Uganda, March 21-24, 2012}, year = {2012}, annote = {No sources available}, pub_type = {conference}, category = {ict4d} }

  17. Ciaghi, A., Eshete, B., Molini, P., & Villafiorita, A. (2012). Social Accountability in {M}ozambique: an Experience Report from the {M}oamba District. In E-Infrastructures and E-Services on Developing Countries: Fourth International ICST and IEEE Conference, AFRICOMM 2012, Yaounde, Cameroon, November 12-14. [Download] [Abstract] Empowering citizens in making Governments more account- able and transparent in the services the provide has gained more atten- tion in the last few years both in the developing and in the developed world. At the basis of any such exercise, information and data collection activities play an important role. In this paper we report on a pilot we conducted in collaboration with the Ministry of Education, the World- Bank, the Maputo Living Lab, in the Moamba region of Mozambique to experiment with a platform we developed to collect data about various procurement indicators of primary schools in the region. @inproceedings{CiaEshMol12, author = {Ciaghi, Aaron and Eshete, Birhanu and Molini, Pietro and Villafiorita, Adolfo}, title = {Social Accountability in {M}ozambique: an Experience Report from the {M}oamba District}, booktitle = {E-Infrastructures and E-Services on Developing Countries: Fourth International ICST and IEEE Conference, AFRICOMM 2012, Yaounde, Cameroon, November 12-14}, year = {2012}, abstract = {Empowering citizens in making Governments more account- able and transparent in the services the provide has gained more atten- tion in the last few years both in the developing and in the developed world. At the basis of any such exercise, information and data collection activities play an important role. In this paper we report on a pilot we conducted in collaboration with the Ministry of Education, the World- Bank, the Maputo Living Lab, in the Moamba region of Mozambique to experiment with a platform we developed to collect data about various procurement indicators of primary schools in the region.}, pub_type = {conference}, category = {ict4d}, link = {http://www.ict4g.net/adolfo/downloads/papers/africomm12-samo.pdf} }

  18. Sahilu, H., Villafiorita, A., Weldemariam, K., Belachew, M., & Zewge, A. (2012). Designing distributed agricultural information services for developing countries. In E. Cutrell, E. W. Zegura, G. Borriello, & B. Thies (Eds.), ACM DEV (p. 24). ACM. [Abstract] In developing countries, agriculture is the largest livelihood provider. Nevertheless, the vast majority of gains by farmers are unsatisfactory despite the efforts put into the agriculture cost inputs. At present smallholder farmers, farmers associations, consumers, intermediaries and supporting organizations (e.g., extension agencies) are often unable to engage effectively in agricultural markets since these markets are prone to inefficiencies. Small and subsistence farmers in particular tend to have unfavorable linkages to markets due to a lack of market orientation. They continue to rely on market information supplied and verified through traditional word-of-mouth approach. Many producers and smaller intermediaries also lack experience to effectively utilize such market information to improve their well-being. @inproceedings{DBLP:conf/dev/SahiluVWBZ12, author = {Sahilu, Henok and Villafiorita, Adolfo and Weldemariam, Komminist and Belachew, Mesfin and Zewge, Amanuel}, title = {Designing distributed agricultural information services for developing countries}, booktitle = {ACM DEV}, year = {2012}, pages = {24}, abstract = {In developing countries, agriculture is the largest livelihood provider. Nevertheless, the vast majority of gains by farmers are unsatisfactory despite the efforts put into the agriculture cost inputs. At present smallholder farmers, farmers associations, consumers, intermediaries and supporting organizations (e.g., extension agencies) are often unable to engage effectively in agricultural markets since these markets are prone to inefficiencies. Small and subsistence farmers in particular tend to have unfavorable linkages to markets due to a lack of market orientation. They continue to rely on market information supplied and verified through traditional word-of-mouth approach. Many producers and smaller intermediaries also lack experience to effectively utilize such market information to improve their well-being.}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/dev/2012}, ee = {http://doi.acm.org/10.1145/2160601.2160631}, pub_type = {conference}, category = {ict4d} }

  19. Ciaghi, A., Valle, A. D., & Villafiorita, A. (2011). Adapting Software Metrics to Analyze the Evolution of Laws – An Italian Case Study. In K. M. Atkinson (Ed.), Frontiers in Artificial Intelligence and Applications (Vol. 235, pp. 53–62). IOS Press. [Download] [Abstract] Law-makers, designers of legal information systems and citizens are often challenged by the complexity of bodies of law and the growing number of references needed to interpret a law. Quantifying this complexity is not an easy task. In this paper we present some analyses we conducted on the Italian body of laws, made available through the Normattiva'' website. Some of the metrics we applied are similar to those often used to measure the quality of software systems.</span> <span class="bibtex">@inproceedings{Ciaghi:2011woa, author = {Ciaghi, Aaron and Valle, Andrea Dalla and Villafiorita, Adolfo}, title = {Adapting Software Metrics to Analyze the Evolution of Laws -- An Italian Case Study}, booktitle = {Frontiers in Artificial Intelligence and Applications}, year = {2011}, editor = {Atkinson, Katie M.}, volume = {235}, pages = {53-62}, month = dec, publisher = {IOS Press}, abstract = {Law-makers, designers of legal information systems and citizens are often challenged by the complexity of bodies of law and the growing number of references needed to interpret a law. Quantifying this complexity is not an easy task. In this paper we present some analyses we conducted on the Italian body of laws, made available through theNormattiva’’ website. Some of the metrics we applied are similar to those often used to measure the quality of software systems.}, pub_type = {conference}, category = {ict4laws}, link = {http://www.ict4g.net/adolfo/downloads/papers/jurix-2011.pdf}, month_numeric = {12} }

  20. Asfaw, B., Bekele, D., Eshete, B., Villafiorita, A., & Weldemariam, K. (2010). Host-based anomaly detection for pervasive medical systems. In CRiSIS (pp. 1–8). IEEE. [Abstract] Intrusion detection systems are deployed on hosts in a computing infrastructure to tackle undesired events in the course of usage of the systems. One of the promising domains of applying intrusion detection is the healthcare domain. A typical healthcare scenario is characterized by high degree of mobility, frequent interruptions and above all demands access to sensitive medical records by concerned stakeholders. Migrating these set of concerns in pervasive healthcare environ- ment where the traditional characteristics are more intensified in terms of uncertainty, one ends up with more challenges on security due to nature of pervasive devices and wireless communication media along with classic security problems for desktop based systems. Despite evolution of automated healthcare services and sophistication of attacks against such services, there is a reasonable lack of techniques, tools and experimental setups for protecting hosts against intrusive actions. This paper presents a contribution to provide a host- based, anomaly modeling and detection approach based on data mining techniques for pervasive healthcare systems. The technique maintains normal usage profile of pervasive healthcare applications and inspects current workflow against normal usage profile so as to classify it as anomalous or normal. The technique is implemented as a prototype with sample data set and the results obtained revealed that the technique is able to perform classification of anomalous activities with acceptable accuracy. @inproceedings{DBLP:conf/crisis/AsfawBEVW10, author = {Asfaw, Biniyam and Bekele, Dawit and Eshete, Birhanu and Villafiorita, Adolfo and Weldemariam, Komminist}, title = {Host-based anomaly detection for pervasive medical systems}, booktitle = {CRiSIS}, year = {2010}, pages = {1-8}, abstract = {Intrusion detection systems are deployed on hosts in a computing infrastructure to tackle undesired events in the course of usage of the systems. One of the promising domains of applying intrusion detection is the healthcare domain. A typical healthcare scenario is characterized by high degree of mobility, frequent interruptions and above all demands access to sensitive medical records by concerned stakeholders. Migrating these set of concerns in pervasive healthcare environ- ment where the traditional characteristics are more intensified in terms of uncertainty, one ends up with more challenges on security due to nature of pervasive devices and wireless communication media along with classic security problems for desktop based systems. Despite evolution of automated healthcare services and sophistication of attacks against such services, there is a reasonable lack of techniques, tools and experimental setups for protecting hosts against intrusive actions. This paper presents a contribution to provide a host- based, anomaly modeling and detection approach based on data mining techniques for pervasive healthcare systems. The technique maintains normal usage profile of pervasive healthcare applications and inspects current workflow against normal usage profile so as to classify it as anomalous or normal. The technique is implemented as a prototype with sample data set and the results obtained revealed that the technique is able to perform classification of anomalous activities with acceptable accuracy.}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/crisis/2010}, ee = {http://dx.doi.org/10.1109/CRISIS.2010.5764923}, pub_type = {conference}, category = {health} }

  21. Eshete, B., Villafiorita, A., & Weldemariam, K. (2011). Early Detection of Security Misconfiguration Vulnerabilities in Web Applications. In ARES (pp. 169–174). IEEE. @inproceedings{DBLP:conf/aresec/EsheteVW11, author = {Eshete, Birhanu and Villafiorita, Adolfo and Weldemariam, Komminist}, title = {Early Detection of Security Misconfiguration Vulnerabilities in Web Applications}, booktitle = {ARES}, year = {2011}, pages = {169-174}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/aresec/2011}, ee = {http://doi.ieeecomputersociety.org/10.1109/ARES.2011.31}, pub_type = {conference}, category = {web_development} }

  22. Ciaghi, A., & Villafiorita, A. (2012). Crowdsourcing ICTD Best Practices. In Springer (Ed.), E-Infrastructures and E-Services on Developing Countries: Third International ICST Conference, AFRICOMM 2011, Zanzibar, Tanzania, November 23-24 (Vol. 92, pp. 167–176). [Download] [Abstract] Most ICT for Development projects fail. We claim that most failures are due to an unstructured approach to software development. In this paper, we propose a crowdsourcing web portal to collect best practices from ICTD project managers and allow them to access a com- mon knowledge base. This will allow us to understand how to improve activities within the lifecycle of projects and design a software process for ICTD. @inproceedings{Ciaghi:2012uq, author = {Ciaghi, Aaron and Villafiorita, Adolfo}, title = {Crowdsourcing ICTD Best Practices}, booktitle = {E-Infrastructures and E-Services on Developing Countries: Third International ICST Conference, AFRICOMM 2011, Zanzibar, Tanzania, November 23-24}, year = {2012}, editor = {Springer}, volume = {92}, series = {LNICST}, pages = {167-176}, month = mar, abstract = {Most ICT for Development projects fail. We claim that most failures are due to an unstructured approach to software development. In this paper, we propose a crowdsourcing web portal to collect best practices from ICTD project managers and allow them to access a com- mon knowledge base. This will allow us to understand how to improve activities within the lifecycle of projects and design a software process for ICTD.}, pub_type = {conference}, category = {ict4d}, link = {http://ict4g.net/adolfo/downloads/papers/africomm11-crowdsourcing.pdf}, month_numeric = {3} }

  23. Ciaghi, A., Villafiorita, A., Chemane, L., & Macueve, G. (2011). Stimulating Development through Transnational Living Labs: the Italo-Mozambican Vision. In Proceedings of the 6th Annual IST-Africa Conference Gabarone, Botswana. [Abstract] In this paper, we present the vision for Maputo Living Lab (MLL), which started in January 2011, as part of a network of Living Labs located in developed and in developing regions. The Maputo Living Lab has the purpose of activating a transfer of competences, innovation and education between Trentino (an Autonomous Province in Northern Italy), Mozambique and other developing countries. The tight connection between Mozambique and Trentino makes some characteristics of MLL unique in the Living Labs panorama and poses various challenges that we describe in this paper. @inproceedings{Ciaghi:2011uq, author = {Ciaghi, Aaron and Villafiorita, Adolfo and Chemane, Lourino and Macueve, Gertrudes}, title = {Stimulating Development through Transnational Living Labs: the Italo-Mozambican Vision}, booktitle = {Proceedings of the 6th Annual IST-Africa Conference Gabarone, Botswana}, year = {2011}, month = may, abstract = {In this paper, we present the vision for Maputo Living Lab (MLL), which started in January 2011, as part of a network of Living Labs located in developed and in developing regions. The Maputo Living Lab has the purpose of activating a transfer of competences, innovation and education between Trentino (an Autonomous Province in Northern Italy), Mozambique and other developing countries. The tight connection between Mozambique and Trentino makes some characteristics of MLL unique in the Living Labs panorama and poses various challenges that we describe in this paper.}, pub_type = {conference}, category = {ict4d}, month_numeric = {5} }

  24. Weldemariam, K., & Villafiorita, A. (2011). A Formal Methodology for Procedural Security Assessment. In Proceedings of the Fifth International Conference on Digital Society. [Abstract] Formal analysis techniques can deliver important support during ICT-based innovation (or redesign) efforts in e-government services. This paper discusses a formal methodology for assessing the procedural security of an organization. We do so by explicitly reasoning on critical information flow named assets flows. With this it is possible to understand how critical assets are modified in unlawful manner, which can trigger security and privacy violations, thereby (automatically) detecting security weaknesses within an organization under evaluation. @inproceedings{Weldemariam:2011fj, author = {Weldemariam, Komminist and Villafiorita, Adolfo}, title = {A Formal Methodology for Procedural Security Assessment}, booktitle = {Proceedings of the Fifth International Conference on Digital Society}, year = {2011}, abstract = {Formal analysis techniques can deliver important support during ICT-based innovation (or redesign) efforts in e-government services. This paper discusses a formal methodology for assessing the procedural security of an organization. We do so by explicitly reasoning on critical information flow named assets flows. With this it is possible to understand how critical assets are modified in unlawful manner, which can trigger security and privacy violations, thereby (automatically) detecting security weaknesses within an organization under evaluation. }, pub_type = {conference}, category = {evoting} }

  25. Ciaghi, A., Weldemariam, K., & Villafiorita, A. (2011). Law Modeling with Ontological Support and BPMN: a Case Study. In Proceedings of the Fifth International Conference on Digital Society - CYBERLAWS. [Abstract] Modeling and analysis of legal documents is becom- ing more widely used in eGovernment practices. To support these activities, various frameworks, standards, and ICT-based tools have been developed in the recent years. These approaches are mostly oriented towards defining common standards, managing legal documents and check compliance with current regulations. Along this line, we have devised a tool-supported methodology that allows to model and analyze laws and procedures within public administrations. The approach used in this paper is based on BPMN for the visualization and formalization of business processes and on OWL-DL for the specification of a business process ontology. In this paper we demonstrate the applicability of our approach by using the part of the Italian Immigration Law concerning Family Reunification as a case study. From this initial investigation, our approach can be used on actual laws that describe or affect procedures. @inproceedings{Ciaghi:2011fj, author = {Ciaghi, Aaron and Weldemariam, Komminist and Villafiorita, Adolfo}, title = {Law Modeling with Ontological Support and BPMN: a Case Study}, booktitle = {Proceedings of the Fifth International Conference on Digital Society - CYBERLAWS}, year = {2011}, abstract = {Modeling and analysis of legal documents is becom- ing more widely used in eGovernment practices. To support these activities, various frameworks, standards, and ICT-based tools have been developed in the recent years. These approaches are mostly oriented towards defining common standards, managing legal documents and check compliance with current regulations. Along this line, we have devised a tool-supported methodology that allows to model and analyze laws and procedures within public administrations. The approach used in this paper is based on BPMN for the visualization and formalization of business processes and on OWL-DL for the specification of a business process ontology. In this paper we demonstrate the applicability of our approach by using the part of the Italian Immigration Law concerning Family Reunification as a case study. From this initial investigation, our approach can be used on actual laws that describe or affect procedures.}, pub_type = {conference}, category = {ict4laws} }

  26. Sartori, V., Eshete, B., & Villafiorita, A. (2011). Measuring the Impact of Different Metrics on Software Quality: a Case Study in the Open Source Domain. In Proceedings of the Fifth International Conference on Digital Society. [Abstract] Knowledge about the expected impact of different project and technological choices is fundamental for project planning, resource allocation, and quality of the final software product. The latter property, in particular, is essential to gain users’ trust and confidence. In this paper we present some preliminary results about a study we are conducting on open source web applications available in SourceForge. The ultimate goal is providing tools to support project managers and team in making choices that, being all other factors the same, increase the probability of delivering higher quality software products. @inproceedings{Sartori:2011qy, author = {Sartori, Valentino and Eshete, Birhanu and Villafiorita, Adolfo}, title = {Measuring the Impact of Different Metrics on Software Quality: a Case Study in the Open Source Domain}, booktitle = {Proceedings of the Fifth International Conference on Digital Society}, year = {2011}, abstract = {Knowledge about the expected impact of different project and technological choices is fundamental for project planning, resource allocation, and quality of the final software product. The latter property, in particular, is essential to gain users’ trust and confidence. In this paper we present some preliminary results about a study we are conducting on open source web applications available in SourceForge. The ultimate goal is providing tools to support project managers and team in making choices that, being all other factors the same, increase the probability of delivering higher quality software products.}, pub_type = {conference}, category = {spm} }

  27. Ciaghi, A., & Villafiorita, A. (2011). Improving Public Administrations via Law Modeling and {BPR}. In Springer (Ed.), E-Infrastructures and E-Services on Developing Countries: Second International ICST Conference, AFRICOMM 2010, Cape Town, South Africa. [Abstract] Semantic Web technologies can be used to produce concep- tual representations of legal documents and to perform reasoning on the information that they contain. At the same time, Business Process Re-engineering is being applied more frequently to optimize the procedures of Public Administrations. While the existing literature on tools and methodologies to analyze, model and manipulate legal documents is extensive, there is a lack of a comprehensive tool that allows for a complete analysis of laws in all their aspect. In this paper we propose the design of a modeling framework to support the law-making process, facilitating the participation of people without a jurisprudence background to the editing of regulations. @inproceedings{Ciaghi:2011fk, author = {Ciaghi, Aaron and Villafiorita, Adolfo}, title = {Improving Public Administrations via Law Modeling and {BPR}}, booktitle = {E-Infrastructures and E-Services on Developing Countries: Second International ICST Conference, AFRICOMM 2010, Cape Town, South Africa}, year = {2011}, editor = {Springer}, month = oct, abstract = {Semantic Web technologies can be used to produce concep- tual representations of legal documents and to perform reasoning on the information that they contain. At the same time, Business Process Re-engineering is being applied more frequently to optimize the procedures of Public Administrations. While the existing literature on tools and methodologies to analyze, model and manipulate legal documents is extensive, there is a lack of a comprehensive tool that allows for a complete analysis of laws in all their aspect. In this paper we propose the design of a modeling framework to support the law-making process, facilitating the participation of people without a jurisprudence background to the editing of regulations.}, pub_type = {conference}, category = {ict4laws}, month_numeric = {10} }

  28. Weldemariam, K., Villafiorita, A., & Mattioli, A. (2009). Experiments and data analysis of electronic voting system. In A. A. E. Kalam, Y. Deswarte, & M. Mostafa (Eds.), CRiSIS (pp. 105–112). IEEE. [Abstract] During the last four years we have been involved in the development, experimentation, and evaluation of an electronic voting (e-voting) system. The system tried out in several regular elections, and also used in two small elections with legal value. Each experiment provided various sociological (e.g. citizens’ opinions on the system) and technical data that are related to system’s performance and behavior. This paper presents various technical insights and the lesson learned during the e-voting experiment. This helps to confirm existing data on the subject (e.g., data related to security, procedures and logistics) and, in some cases, provide novel information or, at least, shed a new perspective on some security-critical factors concerning e-voting systems. @inproceedings{DBLP:conf/crisis/WeldemariamVM09, author = {Weldemariam, Komminist and Villafiorita, Adolfo and Mattioli, Andrea}, title = {Experiments and data analysis of electronic voting system}, booktitle = {CRiSIS}, year = {2009}, pages = {105-112}, abstract = {During the last four years we have been involved in the development, experimentation, and evaluation of an electronic voting (e-voting) system. The system tried out in several regular elections, and also used in two small elections with legal value. Each experiment provided various sociological (e.g. citizens’ opinions on the system) and technical data that are related to system’s performance and behavior. This paper presents various technical insights and the lesson learned during the e-voting experiment. This helps to confirm existing data on the subject (e.g., data related to security, procedures and logistics) and, in some cases, provide novel information or, at least, shed a new perspective on some security-critical factors concerning e-voting systems.}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/crisis/2009}, ee = {http://dx.doi.org/10.1109/CRISIS.2009.5411972}, pub_type = {conference}, category = {evoting} }

  29. Weldemariam, K., Kemmerer, R. A., & Villafiorita, A. (2009). Formal analysis of attacks for e-voting system. In A. A. E. Kalam, Y. Deswarte, & M. Mostafa (Eds.), CRiSIS (pp. 26–34). IEEE. [Abstract] Recently, the use of formal methods to specify and verify properties of electronic voting (e-voting) systems, with particular interest in security, verifiability, and anonymity, is getting much attention. Formal specification and verification of such systems can greatly help to better understand the system requirements by thoroughly specifying and analyzing the underlying assumptions and security specific properties. Unfortunately, even though these systems have been formally verified to satisfy the desired system security requirements, they are still vulnerable to attack. In this paper we extend a formal specification of the ES&S voting system by specifying attacks that have been shown to successfully compromise the system. We believe that performing such analysis is important for two reasons: first, it allows us to discover some missing critical requirements for the specification and/or assumptions that were not met. Second, it allows us to derive mitigation or counter-measure strategies when the system behaves differently than it should. We used the ASTRAL language for the specification, and the verification is performed using the PVS tool. @inproceedings{DBLP:conf/crisis/WeldemariamKV09, author = {Weldemariam, Komminist and Kemmerer, Richard A. and Villafiorita, Adolfo}, title = {Formal analysis of attacks for e-voting system}, booktitle = {CRiSIS}, year = {2009}, pages = {26-34}, abstract = {Recently, the use of formal methods to specify and verify properties of electronic voting (e-voting) systems, with particular interest in security, verifiability, and anonymity, is getting much attention. Formal specification and verification of such systems can greatly help to better understand the system requirements by thoroughly specifying and analyzing the underlying assumptions and security specific properties. Unfortunately, even though these systems have been formally verified to satisfy the desired system security requirements, they are still vulnerable to attack. In this paper we extend a formal specification of the ES&S voting system by specifying attacks that have been shown to successfully compromise the system. We believe that performing such analysis is important for two reasons: first, it allows us to discover some missing critical requirements for the specification and/or assumptions that were not met. Second, it allows us to derive mitigation or counter-measure strategies when the system behaves differently than it should. We used the ASTRAL language for the specification, and the verification is performed using the PVS tool.}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/crisis/2009}, ee = {http://dx.doi.org/10.1109/CRISIS.2009.5411982}, pub_type = {conference}, category = {evoting} }

  30. Weldemariam, K., & Villafiorita, A. (2010). A Survey: Electronic Voting Development and Trends. In R. Krimmer & R. Grimm (Eds.), Electronic Voting (Vol. 167, pp. 119–131). GI. [Abstract] Any practitioner working on electronic voting (e-voting) seem to have stumbled upon the main issues that seem to affect the area. On the one hand —given the criticality and the risk e-voting systems potentially pose to the democratic process— e-voting systems are permanently under a magnifying glass that amplifies any glitch, be it significant or not. On the other hand, given the interest e-voting raises with the general public, there seems to be a tendency to generalize and oversimplify. This tendency leads to attribute specific problems to all systems, regardless of context, situation, and actual systems used. Additionally, scarce know-how about the electoral context often contributes to make matters even more confused. This is not to say all e-voting systems show the security and reliability characteristics that are necessary for system of such a criticality. On the contrary, a lot of work still has to be done. Starting from previous experiences and from a large-scale experimentation we conducted in Italy, this paper provides some directions, issues, and trends in e-voting. Getting a clearer view of the research activities in the area, highlighting both positive and negative results, and emphasizing some trends, could help, in our opinion, drawing a neater line between opinion from facts and contribute to the construction of a next generation of e-voting machines to be safely and more confidently employed for elections. @inproceedings{DBLP:conf/ev/WeldemariamV10, author = {Weldemariam, Komminist and Villafiorita, Adolfo}, title = {A Survey: Electronic Voting Development and Trends}, booktitle = {Electronic Voting}, year = {2010}, pages = {119-131}, abstract = {Any practitioner working on electronic voting (e-voting) seem to have stumbled upon the main issues that seem to affect the area. On the one hand —given the criticality and the risk e-voting systems potentially pose to the democratic process— e-voting systems are permanently under a magnifying glass that amplifies any glitch, be it significant or not. On the other hand, given the interest e-voting raises with the general public, there seems to be a tendency to generalize and oversimplify. This tendency leads to attribute specific problems to all systems, regardless of context, situation, and actual systems used. Additionally, scarce know-how about the electoral context often contributes to make matters even more confused. This is not to say all e-voting systems show the security and reliability characteristics that are necessary for system of such a criticality. On the contrary, a lot of work still has to be done. Starting from previous experiences and from a large-scale experimentation we conducted in Italy, this paper provides some directions, issues, and trends in e-voting. Getting a clearer view of the research activities in the area, highlighting both positive and negative results, and emphasizing some trends, could help, in our opinion, drawing a neater line between opinion from facts and contribute to the construction of a next generation of e-voting machines to be safely and more confidently employed for elections. }, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/ev/2010}, pub_type = {conference}, category = {evoting} }

  31. Villafiorita, A., Weldemariam, K., Susi, A., & Siena, A. (2010). Modeling and Analysis of Laws Using {BPR} and Goal-Oriented Framework. In L. Berntzen, F. Bodendorf, E. Lawrence, M. Perry, & {\AA}sa Smedberg (Eds.), ICDS (pp. 353–358). IEEE Computer Society. [Abstract] Recently, two complementary approaches are proposed to represent, model, and analyze laws: the Nomos and VLPM approaches. Nomos is a goal-oriented approach to effectively capture high-level principles in terms of goal re- alization for requirements guided by satisfiability of normative propositions obtained from rules embedded in a law. The latter offers a tool supported (re-)engineering methodology to extract laws represented in XML and build models using a subset of UML diagrams. Both allow traceability between laws and their respective models. This paper proposes an integration of these two approaches. We believe that this provides a framework that allows to trace and reason either top-down, from principles to their implementation or, viceversa, bottom-up, from a change in the procedure to the principles. It is exactly this connection that adds value to the solution we propose and makes our approach more significant than a simple juxtaposition of the two techniques. @inproceedings{DBLP:conf/icds/VillafioritaWSS10, author = {Villafiorita, Adolfo and Weldemariam, Komminist and Susi, Angelo and Siena, Alberto}, title = {Modeling and Analysis of Laws Using {BPR} and Goal-Oriented Framework}, booktitle = {ICDS}, year = {2010}, pages = {353-358}, note = {Best paper award}, abstract = {Recently, two complementary approaches are proposed to represent, model, and analyze laws: the Nomos and VLPM approaches. Nomos is a goal-oriented approach to effectively capture high-level principles in terms of goal re- alization for requirements guided by satisfiability of normative propositions obtained from rules embedded in a law. The latter offers a tool supported (re-)engineering methodology to extract laws represented in XML and build models using a subset of UML diagrams. Both allow traceability between laws and their respective models. This paper proposes an integration of these two approaches. We believe that this provides a framework that allows to trace and reason either top-down, from principles to their implementation or, viceversa, bottom-up, from a change in the procedure to the principles. It is exactly this connection that adds value to the solution we propose and makes our approach more significant than a simple juxtaposition of the two techniques.}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/icds/2010}, ee = {http://doi.ieeecomputersociety.org/10.1109/ICDS.2010.57}, pub_type = {conference}, category = {ict4laws} }

  32. Bekele, D., Eshete, B., Villafiorita, A., & Weldemariam, K. (2010). Context Information Refinement for Pervasive Medical Systems. In L. Berntzen, F. Bodendorf, E. Lawrence, M. Perry, & {\AA}sa Smedberg (Eds.), ICDS (pp. 210–215). IEEE Computer Society. [Abstract] Emerging technologies like mobile and wireless communication are offering promising opportunities to enable mobile healthcare delivery to citizens. But, enhancing the qual- ity of service of such systems demands systematic improvement of existing service infrastructure. In this paper, we describe a context information refinement architecture proposed to address the shortcomings of existing works in relation to context information refinement in pervasive medical systems. The shortcomings are lack of adequate consideration for: quality parameters of context information, relevance of context information and particular requirements of the pervasive healthcare domain. The proposed architecture facilitates and coordinates the refinement of context infor- mation starting from acquisition of context information up until the refined context information is delivered to the target application in a pervasive medical system. We developed a prototype that implements the core components of the proposed architecture and evaluated it with real-life pervasive healthcare scenario and proved the validity of the architecture using a real-life scenario. @inproceedings{DBLP:conf/icds/BekeleEVW10, author = {Bekele, Dawit and Eshete, Birhanu and Villafiorita, Adolfo and Weldemariam, Komminist}, title = {Context Information Refinement for Pervasive Medical Systems}, booktitle = {ICDS}, year = {2010}, pages = {210-215}, note = {Best paper award}, abstract = {Emerging technologies like mobile and wireless communication are offering promising opportunities to enable mobile healthcare delivery to citizens. But, enhancing the qual- ity of service of such systems demands systematic improvement of existing service infrastructure. In this paper, we describe a context information refinement architecture proposed to address the shortcomings of existing works in relation to context information refinement in pervasive medical systems. The shortcomings are lack of adequate consideration for: quality parameters of context information, relevance of context information and particular requirements of the pervasive healthcare domain. The proposed architecture facilitates and coordinates the refinement of context infor- mation starting from acquisition of context information up until the refined context information is delivered to the target application in a pervasive medical system. We developed a prototype that implements the core components of the proposed architecture and evaluated it with real-life pervasive healthcare scenario and proved the validity of the architecture using a real-life scenario.}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/icds/2010}, ee = {http://doi.ieeecomputersociety.org/10.1109/ICDS.2010.42}, pub_type = {conference}, category = {health} }

  33. Eshete, B., Mattioli, A., Villafiorita, A., & Weldemariam, K. (2010). ICT for Good: Opportunities, Challenges and the Way Forward. In L. Berntzen, F. Bodendorf, E. Lawrence, M. Perry, & {\AA}sa Smedberg (Eds.), ICDS (pp. 14–19). IEEE Computer Society. [Abstract] ICT seems well understood as a tool and an infrastructure for delivering information and services for the society and for allowing communications through interactions among the service users —mostly, the digital society. Using ICT for ensuring better life requires far more than good infrastructure, ICT know-how and the various techniques and tools in place. If ICT has to address the real problems of the society, it should be at a rescue being environment-friendly, with real and tangible impact, sustainable, seamless, down to the grass-roots and above all with reproducible experiences. In this paper, we introduce a different perspective of looking into and using ICT, which we call ICT for Good (ICT4G). It is about using ICT for addressing problems of societies with low ICT penetration and changing a society’s life for the better. More specifically, based on our observation of current promises ICT gives to society, we discuss ICT4G’s distinguishing aspects, opportunities it offers, challenges it imposes along with preliminary roadmap for its realization. A high-level correlation of what we pointed out with a relevant case study (i.e., the eGIF4M1) is presented. @inproceedings{DBLP:conf/icds/EsheteMVW10, author = {Eshete, Birhanu and Mattioli, Andrea and Villafiorita, Adolfo and Weldemariam, Komminist}, title = {ICT for Good: Opportunities, Challenges and the Way Forward}, booktitle = {ICDS}, year = {2010}, pages = {14-19}, abstract = {ICT seems well understood as a tool and an infrastructure for delivering information and services for the society and for allowing communications through interactions among the service users —mostly, the digital society. Using ICT for ensuring better life requires far more than good infrastructure, ICT know-how and the various techniques and tools in place. If ICT has to address the real problems of the society, it should be at a rescue being environment-friendly, with real and tangible impact, sustainable, seamless, down to the grass-roots and above all with reproducible experiences. In this paper, we introduce a different perspective of looking into and using ICT, which we call ICT for Good (ICT4G). It is about using ICT for addressing problems of societies with low ICT penetration and changing a society’s life for the better. More specifically, based on our observation of current promises ICT gives to society, we discuss ICT4G’s distinguishing aspects, opportunities it offers, challenges it imposes along with preliminary roadmap for its realization. A high-level correlation of what we pointed out with a relevant case study (i.e., the eGIF4M1) is presented.}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/icds/2010}, ee = {http://doi.ieeecomputersociety.org/10.1109/ICDS.2010.58}, pub_type = {conference}, category = {ict4d} }

  34. Weldemariam, K., Kemmerer, R. A., & Villafiorita, A. (2010). Formal Specification and Analysis of an E-voting System. In ARES (pp. 164–171). IEEE Computer Society. [Abstract] Electronic voting systems are a perfect example of security-critical computing. One of the critical and complex parts of such systems is the voting process, which is responsible for correctly and securely storing intentions and actions of the voters. Unfortunately, recent studies revealed that various e-voting systems show serious specification, design, and implementation flaws. The application of formal specification and verification can greatly help to better understand the system requirements of e-voting systems by thoroughly specifying and analyzing the underlying assumptions and the security specific properties. This paper presents the specification and verification of the electronic voting process for the Election Systems & Software (ES&S) system. We used the ASTRAL language to specify the voting process of ES&S machines and the critical security requirements for the system. Proof obligations that verify that the specified system meets the critical requirements were automatically generated by the ASTRAL Software Development Environment (SDE). The PVS interactive theorem prover was then used to apply the appropriate proof strategies and discharge the proof obligations. @inproceedings{DBLP:conf/IEEEares/WeldemariamKV10, author = {Weldemariam, Komminist and Kemmerer, Richard A. and Villafiorita, Adolfo}, title = {Formal Specification and Analysis of an E-voting System}, booktitle = {ARES}, year = {2010}, pages = {164-171}, abstract = {Electronic voting systems are a perfect example of security-critical computing. One of the critical and complex parts of such systems is the voting process, which is responsible for correctly and securely storing intentions and actions of the voters. Unfortunately, recent studies revealed that various e-voting systems show serious specification, design, and implementation flaws. The application of formal specification and verification can greatly help to better understand the system requirements of e-voting systems by thoroughly specifying and analyzing the underlying assumptions and the security specific properties. This paper presents the specification and verification of the electronic voting process for the Election Systems & Software (ES&S) system. We used the ASTRAL language to specify the voting process of ES&S machines and the critical security requirements for the system. Proof obligations that verify that the specified system meets the critical requirements were automatically generated by the ASTRAL Software Development Environment (SDE). The PVS interactive theorem prover was then used to apply the appropriate proof strategies and discharge the proof obligations.}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/IEEEares/2010}, ee = {http://doi.ieeecomputersociety.org/10.1109/ARES.2010.83}, pub_type = {conference}, category = {evoting} }

  35. Ciaghi, A., Weldemariam, K., Villafiorita, A., Mattioli, A., & Quoc-Phan, S. (2010). Supporting Public Administration with an Integrated {BPR} Environment. In A. Villafiorita, S.-P. Regis, & A. Zorer (Eds.), E-Infrastructures and E-Services on Developing Countries: First International ICST Conference, AFRICOMM 2009, Maputo, Mozambique. Springer. [Abstract] The definition or redesign of Public Administration (PA) procedures is particularly challenging. This is, for example, due to the requirement of cooperation of different organizational units and actors, different laws and procedures for the production of several artifacts, and maintaining traceability while integrating processes with new laws. We are interested in business process modeling and re-engineering (BPR) for PA, where ICT can play a pivotal role by, e.g., improving communication among law-makers and process analysts. With regard to this previously we developed a tool called VLPM1. The tool is designed to provide assistance in BPR for PA, which allows traceability between laws and processes. In this paper, we discuss the extension of the tool and of its methodology to support an integrated environment that can be used for better law and process redesign by performing formal analysis on the processes. We discuss its system components and provide a working example taken from the Italian Immigration law, as a proof of concept. @inproceedings{Ciaghi:2009xb, author = {Ciaghi, Aaron and Weldemariam, Komminist and Villafiorita, Adolfo and Mattioli, Andrea and Quoc-Phan, Sang}, title = {Supporting Public Administration with an Integrated {BPR} Environment}, booktitle = {E-Infrastructures and E-Services on Developing Countries: First International ICST Conference, AFRICOMM 2009, Maputo, Mozambique}, year = {2010}, editor = {Villafiorita, Adolfo and Regis, Saint-Paul and Zorer, Alessandro}, month = jun, publisher = {Springer}, abstract = {The definition or redesign of Public Administration (PA) procedures is particularly challenging. This is, for example, due to the requirement of cooperation of different organizational units and actors, different laws and procedures for the production of several artifacts, and maintaining traceability while integrating processes with new laws. We are interested in business process modeling and re-engineering (BPR) for PA, where ICT can play a pivotal role by, e.g., improving communication among law-makers and process analysts. With regard to this previously we developed a tool called VLPM1. The tool is designed to provide assistance in BPR for PA, which allows traceability between laws and processes. In this paper, we discuss the extension of the tool and of its methodology to support an integrated environment that can be used for better law and process redesign by performing formal analysis on the processes. We discuss its system components and provide a working example taken from the Italian Immigration law, as a proof of concept.}, pub_type = {conference}, category = {ict4laws}, month_numeric = {6} }

  36. Shvaiko, P., Villafiorita, A., Zorer, A., Chemane, L., Fumo, T., & Hinkkanen, J. (2009). eGIF4M: eGovernment Interoperability Framework for Mozambique. In M. Wimmer, H. J. Scholl, M. Janssen, & R. Traunm{"u}ller (Eds.), EGOV (Vol. 5693, pp. 328–340). Springer. [Download] [Abstract] Harmonizing decentralized development of ICT solutions with centralized strategies, e.g., meant to favor reuse and optimization of re- sources, is a complex technical and organizational challenge. The prob- lem, shared by virtually all the governments, is becoming a priority also for countries, such as Mozambique, that have started their ICT policy relatively recently and for which it is now evident that — if no particular attention is devoted to the interoperability of the solutions being developed — the result will rapidly become a patchwork of solutions incompatible with each other. This paper presents eGIF4M: eGovernment Interoperability Framework for Mozambique. The framework is based on a holistic approach. It builds on top of the existing experiences in eGIFs all over the world and it addresses some specific needs and peculiarities of developing countries, like Mozambique. The result is a comprehensive framework based on: (i) a reference architecture along with technical standards, (ii) a standardization life cycle, (iii) a maturity model, and (iv) some key actions meant to make the initiative sustainable in the longer term. @inproceedings{DBLP:conf/egov/ShvaikoVZCFH09, author = {Shvaiko, Pavel and Villafiorita, Adolfo and Zorer, Alessandro and Chemane, Lourino and Fumo, Teot{'o}nio and Hinkkanen, Jussi}, title = {eGIF4M: eGovernment Interoperability Framework for Mozambique}, booktitle = {EGOV}, year = {2009}, pages = {328-340}, abstract = {Harmonizing decentralized development of ICT solutions with centralized strategies, e.g., meant to favor reuse and optimization of re- sources, is a complex technical and organizational challenge. The prob- lem, shared by virtually all the governments, is becoming a priority also for countries, such as Mozambique, that have started their ICT policy relatively recently and for which it is now evident that — if no particular attention is devoted to the interoperability of the solutions being developed — the result will rapidly become a patchwork of solutions incompatible with each other. This paper presents eGIF4M: eGovernment Interoperability Framework for Mozambique. The framework is based on a holistic approach. It builds on top of the existing experiences in eGIFs all over the world and it addresses some specific needs and peculiarities of developing countries, like Mozambique. The result is a comprehensive framework based on: (i) a reference architecture along with technical standards, (ii) a standardization life cycle, (iii) a maturity model, and (iv) some key actions meant to make the initiative sustainable in the longer term.}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/egov/2009}, ee = {http://dx.doi.org/10.1007/978-3-642-03516-6_28}, pub_type = {conference}, category = {egov4dev_countries}, link = {http://ict4g.net/adolfo/downloads/papers/egif4m-2009.pdf} }

  37. Weldemariam, K. S., & Villafiorita, A. (2008). A Methodology for Assessing Procedural Security: A Case Study in E-Voting. In Electronic Voting (pp. 83–94). GI. [Abstract] The organization of elections in Italy involves various offices of the Public Administration and private contractors, has a time-span of months, and has strict security and traceability requirements. Sensibility by citizens and politicians is very high, and litigation over, e.g., implementation of procedures and validity of results are not uncommon. In this paper we present a methodology for procedural security assessment in order to analyze and eventually make election secure. Our approach is based on modeling the nominal procedures implementation in the form of business process models (which we write in a strict simplified subset of UML), systematically translate the models into executable specification and perform the analysis. We believe such an analysis to be essential to identify the limits of the current procedures (i.e. undetected attacks) and to identify more precisely under what hypotheses we can guaran- tee secure elections. We demonstrate our approach with the help of an excerpt of e-Voting system scenario that it is derived from the current experimentation of the Italian legislation. @inproceedings{Weldemariam:2008ee, author = {Weldemariam, Komminist Sisai and Villafiorita, Adolfo}, title = {A Methodology for Assessing Procedural Security: A Case Study in E-Voting}, booktitle = {Electronic Voting}, year = {2008}, series = {Lecture Notes in Informatics (LNI)}, pages = {83–94}, publisher = {GI}, abstract = {The organization of elections in Italy involves various offices of the Public Administration and private contractors, has a time-span of months, and has strict security and traceability requirements. Sensibility by citizens and politicians is very high, and litigation over, e.g., implementation of procedures and validity of results are not uncommon. In this paper we present a methodology for procedural security assessment in order to analyze and eventually make election secure. Our approach is based on modeling the nominal procedures implementation in the form of business process models (which we write in a strict simplified subset of UML), systematically translate the models into executable specification and perform the analysis. We believe such an analysis to be essential to identify the limits of the current procedures (i.e. undetected attacks) and to identify more precisely under what hypotheses we can guaran- tee secure elections. We demonstrate our approach with the help of an excerpt of e-Voting system scenario that it is derived from the current experimentation of the Italian legislation.}, pub_type = {conference}, location = {Bregenz, Austria}, category = {evoting} }

  38. Weldemariam, K. S., & Villafiorita, A. (2008). Formal Procedural Security Modeling and Analysis. In Proceedings of 3rd International Conference on Risks and Security of Internet and Systems (CriSiS’08) (pp. 249–254). IEEE. [Abstract] We are involved in a project related to the evaluation and possible introduction of e-voting for elections held in the Autonomous Province of Trento. One of the goals of the project is defining the laws and the procedures that will regulate e-voting and guarantee the same or an higher level of security than the traditional, paper-based, elections. To do so, we are tackling the problem (also) at the procedural level, namely, we are trying to understand weaknesses and strengths of the procedures regulating elections in Italy, in order to analyze possible attacks and their effects. The analyses are based on formal specifications of the procedures and on model checkers to help us derive possible attacks. We believe the approach to be useful to help us systematically identifying the limits of the current procedures (i.e. under what hypotheses attacks are undetectable) and, con- sequently, to state more precisely under what hypotheses and conditions we can guarantee reasonably secure elections. @inproceedings{Weldemariam:2008qf, author = {Weldemariam, Komminist Sisai and Villafiorita, Adolfo}, title = {Formal Procedural Security Modeling and Analysis}, booktitle = {Proceedings of 3rd International Conference on Risks and Security of Internet and Systems (CriSiS’08)}, year = {2008}, pages = {249–254}, publisher = {IEEE}, annote = {Publik Printout available}, abstract = {We are involved in a project related to the evaluation and possible introduction of e-voting for elections held in the Autonomous Province of Trento. One of the goals of the project is defining the laws and the procedures that will regulate e-voting and guarantee the same or an higher level of security than the traditional, paper-based, elections. To do so, we are tackling the problem (also) at the procedural level, namely, we are trying to understand weaknesses and strengths of the procedures regulating elections in Italy, in order to analyze possible attacks and their effects. The analyses are based on formal specifications of the procedures and on model checkers to help us derive possible attacks. We believe the approach to be useful to help us systematically identifying the limits of the current procedures (i.e. under what hypotheses attacks are undetectable) and, con- sequently, to state more precisely under what hypotheses and conditions we can guarantee reasonably secure elections.}, pub_type = {conference}, location = {Tozeur, Tunisia}, category = {evoting} }

  39. Weldemariam, K. S., Villafiorita, A., & Mattioli, A. (2007). Assessing Procedural Risks and Threats in e-Voting: Challenges and an Approach. In E-Voting and Identity, First International Conference, VOTE-ID 2007 (Vol. 4896, pp. 38–49). Springer Berlin / Heidelberg: Springer. [Abstract] Performing a good security analysis on the design of a system is an essential step in order to guarantee a reasonable level of protection. However, different attacks and threats may be carried out depending on the operational environment in which the system is used, i.e. the pro- cedures that define how to operate the systems. Using strong-passwords to limit access to a system is useless — to make a simple example — if users are allowed to write the passwords on paper and leave them near the computers they operate. We are interested in reasoning about the security of e-Voting procedures, namely on the risks and attacks that can be carried out during an elec- tion. Our focus is more on people and organizations than on systems and technologies. In this paper we describe some ongoing work that we are carrying out within the ProVotE project (a project sponsored by the Autonomous Province of Trento to switch to e-Voting for local elections) to analyze and (possibly) improve procedural security of electronic elections. To do so, we are we are providing models of the Italian electoral laws using the UML and we are developing a custom methodology for analyzing threats from the models. Our reasoning approach is based on asset mobility, asset values and existence of multiple instances. @inproceedings{Weldemariam:2007hq, author = {Weldemariam, Komminist Sisai and Villafiorita, Adolfo and Mattioli, Andrea}, title = {Assessing Procedural Risks and Threats in e-Voting: Challenges and an Approach}, booktitle = {E-Voting and Identity, First International Conference, VOTE-ID 2007}, year = {2007}, volume = {4896}, series = {Lecture Notes in Computer Science}, pages = {38–49}, address = {Springer Berlin / Heidelberg}, publisher = {Springer}, annote = {Publik Printout NOT available}, abstract = {Performing a good security analysis on the design of a system is an essential step in order to guarantee a reasonable level of protection. However, different attacks and threats may be carried out depending on the operational environment in which the system is used, i.e. the pro- cedures that define how to operate the systems. Using strong-passwords to limit access to a system is useless — to make a simple example — if users are allowed to write the passwords on paper and leave them near the computers they operate. We are interested in reasoning about the security of e-Voting procedures, namely on the risks and attacks that can be carried out during an elec- tion. Our focus is more on people and organizations than on systems and technologies. In this paper we describe some ongoing work that we are carrying out within the ProVotE project (a project sponsored by the Autonomous Province of Trento to switch to e-Voting for local elections) to analyze and (possibly) improve procedural security of electronic elections. To do so, we are we are providing models of the Italian electoral laws using the UML and we are developing a custom methodology for analyzing threats from the models. Our reasoning approach is based on asset mobility, asset values and existence of multiple instances.}, isbn = {978-3-540-77492-1}, pub_type = {conference}, category = {evoting} }

  40. Weldemariam, K. S., & Villafiorita, A. (2008). Modeling and Analysis of Procedural Security in (e)Voting: the Trentino’s Approach and Experiences. In Proceedings of the conference on Electronic voting technology (pp. 1–10). Berkeley, CA, USA: USENIX Association. [Download] [Abstract] This paper describes the experiences and the challenges we are facing within the ProVotE project, a four years project sponsored by the Autonomous Province of Trento that has the goal of switching to e-voting for local elections. One of the activities we are carrying out within ProVotE is the systematic analysis of the weaknesses and strengths of the procedures regulating local elections in Italy, in order to derive possible attacks and their effects. The approach we take is based on providing formal specifications of the procedures and using model checkers to help us analyze the effects of attacks. We believe such an analysis to be essential to identify the limits of the current procedures (i.e. under what hypotheses attacks are undetectable) and to identify more precisely under what hypotheses and conditions we can guarantee reasonably secure electronic elections. This paper presents the methodology and the techniques we are devising and experimenting with to tackle problem highlighted above. @inproceedings{Weldemariam:2008ay, author = {Weldemariam, Komminist Sisai and Villafiorita, Adolfo}, title = {Modeling and Analysis of Procedural Security in (e)Voting: the Trentino’s Approach and Experiences}, booktitle = {Proceedings of the conference on Electronic voting technology}, year = {2008}, pages = {1–10}, address = {Berkeley, CA, USA}, publisher = {USENIX Association}, annote = {Publik Printout available on the internet}, abstract = {This paper describes the experiences and the challenges we are facing within the ProVotE project, a four years project sponsored by the Autonomous Province of Trento that has the goal of switching to e-voting for local elections. One of the activities we are carrying out within ProVotE is the systematic analysis of the weaknesses and strengths of the procedures regulating local elections in Italy, in order to derive possible attacks and their effects. The approach we take is based on providing formal specifications of the procedures and using model checkers to help us analyze the effects of attacks. We believe such an analysis to be essential to identify the limits of the current procedures (i.e. under what hypotheses attacks are undetectable) and to identify more precisely under what hypotheses and conditions we can guarantee reasonably secure electronic elections. This paper presents the methodology and the techniques we are devising and experimenting with to tackle problem highlighted above.}, pub_type = {conference}, location = {San Jose, USA}, category = {evoting}, link = {https://www.usenix.org/legacy/event/evt08/tech/full_papers/weldemariam/weldemariam.pdf} }

  41. Sebastiani, R., & Villafiorita, A. (1998). SAT-based decision procedures for normal modal logics: a theoretical framework. In Proceedings of 8th International Conference on Artificial Intelligence: Methodology, Systems, and Applications (AIMSA98). Springer. @inproceedings{Sebastiani:1998dw, author = {Sebastiani, Roberto and Villafiorita, Adolfo}, title = {SAT-based decision procedures for normal modal logics: a theoretical framework}, booktitle = {Proceedings of 8th International Conference on Artificial Intelligence: Methodology, Systems, and Applications (AIMSA98)}, year = {1998}, publisher = {Springer}, annote = {Publik Printout available}, pub_type = {conference}, location = {Sozopol, Bulgaria}, category = {theorem_proving} }

  42. Bozzano, M., & Villafiorita, A. (2003). Improving System Reliability via Model Checking: the {FSAP/NuSMV-SA} Safety Analysis Platform. In Proceedings of the 22nd International Confecence SAFECOMP 2003 (Vol. 2788, pp. 49–62). Springer. [Abstract] Safety critical systems are becoming more complex, both in the type of functionality they provide and in the way they are demanded to interact with their environment. Such growing complexity requires an adequate increase in the capability of safety engineers to assess system safety, including analyzing the bahaviour of a system in degraded situations. Formal verification techniques, like symbolic model checking, have the potential of dealing with such a complexity and are more often being used during system design. In this paper we present the FSAP/NuSMV- SA platform, based on the NuSMV2 model checker, that implements known and novel techniques to help safety engineers perform safety analysis. The main functionality of FSAP/NuSMV-SA include: failure mode definition based on a library of failure modes, fault injection, automatic fault tree construction for monotonic and non-monotonic systems, failure ordering analysis. The goal is to provide an environment that can be used both by design engineers to formally verify a system and by safety engineers to automate certain phases of safety assessment. The platform is being developed within the ESACS project (Enhanced Safety Analy- sis for Complex Systems), an European-Union-sponsored project in the avionics sector, whose goal is to define a methodology to improve the safety analysis practice for complex systems development. @inproceedings{Bozzano:2003bl, author = {Bozzano, Marco and Villafiorita, Adolfo}, title = {Improving System Reliability via Model Checking: the {FSAP/NuSMV-SA} Safety Analysis Platform}, booktitle = {Proceedings of the 22nd International Confecence SAFECOMP 2003}, year = {2003}, volume = {2788}, series = {Lecture Notes in Computer Science}, pages = {49–62}, publisher = {Springer}, annote = {Publik Printout available}, abstract = {Safety critical systems are becoming more complex, both in the type of functionality they provide and in the way they are demanded to interact with their environment. Such growing complexity requires an adequate increase in the capability of safety engineers to assess system safety, including analyzing the bahaviour of a system in degraded situations. Formal verification techniques, like symbolic model checking, have the potential of dealing with such a complexity and are more often being used during system design. In this paper we present the FSAP/NuSMV- SA platform, based on the NuSMV2 model checker, that implements known and novel techniques to help safety engineers perform safety analysis. The main functionality of FSAP/NuSMV-SA include: failure mode definition based on a library of failure modes, fault injection, automatic fault tree construction for monotonic and non-monotonic systems, failure ordering analysis. The goal is to provide an environment that can be used both by design engineers to formally verify a system and by safety engineers to automate certain phases of safety assessment. The platform is being developed within the ESACS project (Enhanced Safety Analy- sis for Complex Systems), an European-Union-sponsored project in the avionics sector, whose goal is to define a methodology to improve the safety analysis practice for complex systems development.}, pub_type = {conference}, location = {Edinburgh, Scotland}, category = {safety_analysis} }

  43. Volha, B., Dalpiaz, F., Ferrario, R., Mattioli, A., & Villafiorita, A. (2007). Evaluating Procedural Alternatives: a case study in e-voting. In Proceedings of 1st International Conference on Methodologies, Technologies and Tools Enabling e-Government (MeTTeG07) (pp. 125–138). Halley. [Abstract] This paper describes part of the work carried out within the ProVotE project. It presents the approach we are taking in order to provide both precise models of the electoral processes of an electronic voting, and mechanisms for documenting and reasoning on the possible alternative implementations of the procedures to support the provincial elections of 2008. In particular, the approach is based on defining an alternating sequence of models, written using UML and Tropos. The former is used to represent the electoral processes (both existing and future), while the latter is meant to provide design rationale for the taken decisions about the future procedures. The choice is made after having evaluated the available alternatives against non-functional requirements with the help of Tropos goal analysis techniques. @inproceedings{Volha:2007bv, author = {Volha, Bryl and Dalpiaz, Fabiano and Ferrario, Roberta and Mattioli, Andrea and Villafiorita, Adolfo}, title = {Evaluating Procedural Alternatives: a case study in e-voting}, booktitle = {Proceedings of 1st International Conference on Methodologies, Technologies and Tools Enabling e-Government (MeTTeG07)}, year = {2007}, pages = {125–138}, month = sep, publisher = {Halley}, annote = {Publik Printout available}, abstract = {This paper describes part of the work carried out within the ProVotE project. It presents the approach we are taking in order to provide both precise models of the electoral processes of an electronic voting, and mechanisms for documenting and reasoning on the possible alternative implementations of the procedures to support the provincial elections of 2008. In particular, the approach is based on defining an alternating sequence of models, written using UML and Tropos. The former is used to represent the electoral processes (both existing and future), while the latter is meant to provide design rationale for the taken decisions about the future procedures. The choice is made after having evaluated the available alternatives against non-functional requirements with the help of Tropos goal analysis techniques.}, pub_type = {conference}, category = {evoting}, month_numeric = {9} }

  44. Ciaghi, A., Mattioli, A., & Villafiorita, A. (2009). {VLPM}: a Tool to support {BPR} in Public Administration. In Proceedings of the Third International Conference on Digital Society (ICDS2009) (pp. 289–293). IEEE Computer Society. [Abstract] Representing a law defining some procedures by means of workflow diagrams has various advantages: it facilitates the understanding of the actual meaning of its text, it helps to build a shared vision between law-makers and officers of the Public Administration, and it provides an easier way to analyze and make Public Administration procedures more efficient. To keep the model understandable and maintainable, however, the need soon arises to keep traceability between the workflow diagrams and the laws from which the workflows are derived. Moreover – since the public administration processes are defined and regulated by laws – when the workflows are the target of a re-engineering activity, such traceability information becomes essential to identify what laws need to be changed to implement the new procedures. This paper presents VLPM (Visual Law Process Modeler). It is a tool that addresses some of the issues mentioned above and that we have used to model the laws regulating the introduction of an electronic election in Friuli Venezia Giulia, one of the Autonomous Regions of Italy. VLPM is built on top of the UML Visual Paradigm tool and it is freely available @inproceedings{Ciaghi:2009os, author = {Ciaghi, Aaron and Mattioli, Andrea and Villafiorita, Adolfo}, title = {{VLPM}: a Tool to support {BPR} in Public Administration}, booktitle = {Proceedings of the Third International Conference on Digital Society (ICDS2009)}, year = {2009}, pages = {289–293}, publisher = {IEEE Computer Society}, note = {Best paper award}, annote = {Publik Printout NOT available}, abstract = {Representing a law defining some procedures by means of workflow diagrams has various advantages: it facilitates the understanding of the actual meaning of its text, it helps to build a shared vision between law-makers and officers of the Public Administration, and it provides an easier way to analyze and make Public Administration procedures more efficient. To keep the model understandable and maintainable, however, the need soon arises to keep traceability between the workflow diagrams and the laws from which the workflows are derived. Moreover – since the public administration processes are defined and regulated by laws – when the workflows are the target of a re-engineering activity, such traceability information becomes essential to identify what laws need to be changed to implement the new procedures. This paper presents VLPM (Visual Law Process Modeler). It is a tool that addresses some of the issues mentioned above and that we have used to model the laws regulating the introduction of an electronic election in Friuli Venezia Giulia, one of the Autonomous Regions of Italy. VLPM is built on top of the UML Visual Paradigm tool and it is freely available}, pub_type = {conference}, location = {Cancun, Mexico}, category = {ict4laws} }

  45. Giunchiglia, F., & Villafiorita, A. (1996). ABSFOL: A Proof Checker with Abstraction. In Proceedings of the 13th International Conference on Automated Deduction (CADE13) (Vol. 1104, pp. 136–140). Springer. [Abstract] Intuitively, an abstraction is a mapping from a representation of a problem onto a new representation. ABSFOL is an interactive theorem built on top of GETFOL that supports abstraction. In this paper we demonstrate the use of the tool through an example taken from Boolean Algebra. @inproceedings{Giunchiglia:1996jo, author = {Giunchiglia, Fausto and Villafiorita, Adolfo}, title = {ABSFOL: A Proof Checker with Abstraction}, booktitle = {Proceedings of the 13th International Conference on Automated Deduction (CADE13)}, year = {1996}, volume = {1104}, series = {Lecture Notes in Artificial Intelligence}, pages = {136–140}, month = jul, publisher = {Springer}, annote = {Publik Printout available}, abstract = {Intuitively, an abstraction is a mapping from a representation of a problem onto a new representation. ABSFOL is an interactive theorem built on top of GETFOL that supports abstraction. In this paper we demonstrate the use of the tool through an example taken from Boolean Algebra.}, pub_type = {conference}, location = {New Brunswick, NJ, USA}, category = {theorem_proving}, month_numeric = {7} }

  46. Chiappini, A., Cimatti, A., Porzia, C., Rotondo, G., Sebastiani, R., Traverso, P., & Villafiorita, A. (1999). Formal Specification and Development of a Safety-Critical Train Management. In Proceedings of 18th International Conference on Computer Safety, Reliability and Security (SAFECOMP 1999) (pp. 410–419). Springer. [Abstract] In this paper we describe the on-going specification and development of Ansaldo’s Radio Block Center (RBC), a component of the next-generation European Rail Traffic Management System (ERTMS). The RBC will be responsible of managing the movement of trains equipped with radio communication. Its development process is critical: the RBC is a large-scale and complex system, it must provide several novel services at different levels of functionality, it must guarantee interoperability according to European standards, and, last but not least, a high level of safety. We have addressed these issues by devising a development based on formal specifications. ERTMS scenarios have been formalized in order to provide a better understanding of the interoperability requirements. The architecture of the RBC has been formally specified such that the system can be incrementally built as an overlay system (compatible with the existing train detection and interlocking systems) and modularly expanded to control different kinds of trains. The formal specifications of the behaviour of each RBC module have been structured hierarchically: they provide an easy-to-understand documentation for customers and developers; moreover, they can be simulated and validated automatically at the early stage of the development process, thus providing a high level of confidence in their safety in a cost-effective way. @inproceedings{Chiappini:1999dk, author = {Chiappini, Angelo and Cimatti, Alessandro and Porzia, Carmen and Rotondo, Gianni and Sebastiani, Roberto and Traverso, Paolo and Villafiorita, Adolfo}, title = {Formal Specification and Development of a Safety-Critical Train Management}, booktitle = {Proceedings of 18th International Conference on Computer Safety, Reliability and Security (SAFECOMP 1999)}, year = {1999}, pages = {410–419}, month = sep, publisher = {Springer}, annote = {Publik Printout available}, abstract = {In this paper we describe the on-going specification and development of Ansaldo’s Radio Block Center (RBC), a component of the next-generation European Rail Traffic Management System (ERTMS). The RBC will be responsible of managing the movement of trains equipped with radio communication. Its development process is critical: the RBC is a large-scale and complex system, it must provide several novel services at different levels of functionality, it must guarantee interoperability according to European standards, and, last but not least, a high level of safety. We have addressed these issues by devising a development based on formal specifications. ERTMS scenarios have been formalized in order to provide a better understanding of the interoperability requirements. The architecture of the RBC has been formally specified such that the system can be incrementally built as an overlay system (compatible with the existing train detection and interlocking systems) and modularly expanded to control different kinds of trains. The formal specifications of the behaviour of each RBC module have been structured hierarchically: they provide an easy-to-understand documentation for customers and developers; moreover, they can be simulated and validated automatically at the early stage of the development process, thus providing a high level of confidence in their safety in a cost-effective way. }, pub_type = {conference}, location = {Toulouse, France}, category = {formal_methods}, month_numeric = {9} }

  47. Longo, F., Tiella, R., Tonella, P., & Villafiorita, A. (2008). Measuring the Impact of Different Categories of Software Evolution. In IWSM/Metrikon/Mensura (Vol. 5338, pp. 344–351). Springer. [Abstract] Software evolution involves different categories of interventions, having variable impact on the code. Knowledge about the expected impact of an intervention is fundamental for project planning and resource allocation. Moreover, deviations from the expected impact may hint for areas of the system having a poor design. In this paper, we investigate the relationship between evolution categories and impacted code by means of a set of metrics computed over time for a subject system @inproceedings{Longo:2008jw, author = {Longo, Francesca and Tiella, Roberto and Tonella, Paolo and Villafiorita, Adolfo}, title = {Measuring the Impact of Different Categories of Software Evolution}, booktitle = {IWSM/Metrikon/Mensura}, year = {2008}, volume = {5338}, series = {Lecture Notes in Computer Science}, pages = {344–351}, publisher = {Springer}, annote = {Publik Printout NOT available}, abstract = {Software evolution involves different categories of interventions, having variable impact on the code. Knowledge about the expected impact of an intervention is fundamental for project planning and resource allocation. Moreover, deviations from the expected impact may hint for areas of the system having a poor design. In this paper, we investigate the relationship between evolution categories and impacted code by means of a set of metrics computed over time for a subject system }, pub_type = {conference}, location = {Munich, Germany}, category = {spm} }

  48. Giunchiglia, F., Sebastiani, R., Villafiorita, A., & Walsh, T. (1996). A General Purpose Reasoner for Abstraction. In Proceedings of Advances in Artificial Intelligence, 11th Biennal Conference of the Canadian Society for Computational Studies of Intelligence (AI96) (Vol. 1081, pp. 323–335). Springer. [Abstract] The goal of the work described in this paper is the development of a system, called ABSFOL, which allows the user to state declaratively abstractions and to use them according to the desired control strategy. ABSFOL has been successfully tested on many examples. So far we have failed to find an interesting abstraction whose implementation requires a major programming effort. @inproceedings{Giunchiglia:1996yo, author = {Giunchiglia, Fausto and Sebastiani, Roberto and Villafiorita, Adolfo and Walsh, Toby}, title = {A General Purpose Reasoner for Abstraction}, booktitle = {Proceedings of Advances in Artificial Intelligence, 11th Biennal Conference of the Canadian Society for Computational Studies of Intelligence (AI96)}, year = {1996}, volume = {1081}, series = {Lecture Notes in Artificial Intelligence}, pages = {323–335}, month = may, publisher = {Springer}, annote = {Publik Printout available}, abstract = {The goal of the work described in this paper is the development of a system, called ABSFOL, which allows the user to state declaratively abstractions and to use them according to the desired control strategy. ABSFOL has been successfully tested on many examples. So far we have failed to find an interesting abstraction whose implementation requires a major programming effort.}, pub_type = {conference}, location = {Toronto, Ontario, Canada}, category = {theorem_proving}, month_numeric = {5} }

  49. Bozzano, M., Cavallo, A., Cifaldi, M., Valacca, L., & Villafiorita, A. (2003). Improving Safety Assessment of Complex Systems: An Industrial case study. In Proceedings of the International Symposium of Formal Methods Europe (FME 2003) (Vol. 2805, pp. 208–222). Springer-Verlag. [Abstract] The complexity of embedded controllers is steadily increasing. This trend, stimulated by the continuous improvement of the computational power of hardware, demands for a corresponding increase in the capability of design and safety engineers to maintain adequate safety levels. The use of formal methods during system design has proved to be effective in several practical applications. The development of certain classes of applications, like, for instance, avionic system, however, also requires to analyse the behaviour of a system under certain degraded situations (e.g. when some components are not working as expected). This step, usually performed by safety engineers in a set of dedicated activities, has the goal of pointing out what are all the possible causes of a system malfunction or, more properly, a hazard of the system. It is an essential step to obtain the high safety levels required to keep public confidence in system behaviour, according to the current procedures for system certification (e.g., ARP4754). The integration of system design activities with safety assessment and the use of formal notations for the safety assessment of a system, although not new, are still at an early stage. These goals are addressed by the ESACS project, a European-Union-sponsored project grouping several industrial companies from the aeronautic field. The ESACS project is developing a methodology and a platform the ESACS platform that helps safety engineers automating certain phases of their work. An integral part of the project is the evaluation of the methodology and of the platform on a set of industrial case studies. This paper reports on the application of the ESACS methodology and on the use of the ESACS platform to one of such case studies, namely, the Secondary Power System of the Eurofighter Typhoon aircraft. @inproceedings{Bozzano:2003vh, author = {Bozzano, Marco and Cavallo, Antonella and Cifaldi, Massimo and Valacca, Laura and Villafiorita, Adolfo}, title = {Improving Safety Assessment of Complex Systems: An Industrial case study}, booktitle = {Proceedings of the International Symposium of Formal Methods Europe (FME 2003)}, year = {2003}, volume = {2805}, series = {Lecture Notes in Computer Science}, pages = {208–222}, publisher = {Springer-Verlag}, annote = {Publik Printout available}, abstract = {The complexity of embedded controllers is steadily increasing. This trend, stimulated by the continuous improvement of the computational power of hardware, demands for a corresponding increase in the capability of design and safety engineers to maintain adequate safety levels. The use of formal methods during system design has proved to be effective in several practical applications. The development of certain classes of applications, like, for instance, avionic system, however, also requires to analyse the behaviour of a system under certain degraded situations (e.g. when some components are not working as expected). This step, usually performed by safety engineers in a set of dedicated activities, has the goal of pointing out what are all the possible causes of a system malfunction or, more properly, a hazard of the system. It is an essential step to obtain the high safety levels required to keep public confidence in system behaviour, according to the current procedures for system certification (e.g., ARP4754). The integration of system design activities with safety assessment and the use of formal notations for the safety assessment of a system, although not new, are still at an early stage. These goals are addressed by the ESACS project, a European-Union-sponsored project grouping several industrial companies from the aeronautic field. The ESACS project is developing a methodology and a platform the ESACS platform that helps safety engineers automating certain phases of their work. An integral part of the project is the evaluation of the methodology and of the platform on a set of industrial case studies. This paper reports on the application of the ESACS methodology and on the use of the ESACS platform to one of such case studies, namely, the Secondary Power System of the Eurofighter Typhoon aircraft.}, pub_type = {conference}, location = {Pisa, Italy}, category = {safety_analysis} }

  50. Bozzano, M., Villafiorita, A., Akerlund, O., Bieber, P., Bougnol, C., Boede, E., … Cifaldi, M. (2003). {ESACS}: an integrated methodology for design and safety analysis of complex systems. In Proceedings of the European Safety and Reliability Conference 2003, ESREL2003. Balkema. [Abstract] The continuous increase of system complexity — stimulated by the higher complexity of the functionality provided by software-based embedded controllers and by the huge improvement in the computational power of hardware — requires a corresponding increase in the capability of design and safety engineers to maintain adequate safety and reliability levels. Emerging techniques, like formal methods, have the potential of dealing with the growing complexity of such systems and are increasingly being used for the development of critical systems (e.g. aircraft systems, nuclear plants, railways systems), where at stake are not only delays in delivering products and economical losses, but also environmental hazards and public confidence. However, the use of formal meth- ods during certain critical system development phases, e.g. safety analysis, is still at an early stage. In this paper we propose a new methodology, based on these novel techniques and supported by commercial and state-of-the-art tools, whose goal is to improve the safety analysis practices carried out during the development and certification of complex systems. The key ingredient of our methodology is the use of formal methods during both system development and safety analysis. This allows for a tighter integration of safety assessment and system development activities, fast system prototyping, automated safety assessment since the early stages of development, and tool- supported verification and validation. @inproceedings{Bozzano:2003fe, author = {Bozzano, Marco and Villafiorita, Adolfo and Akerlund, Ove and Bieber, Pierre and Bougnol, C. and Boede, Eckard and Bretschneider, Matthias and Cavallo, Antonella and Castel, C. and Cifaldi, Massimo}, title = {{ESACS}: an integrated methodology for design and safety analysis of complex systems}, booktitle = {Proceedings of the European Safety and Reliability Conference 2003, ESREL2003}, year = {2003}, publisher = {Balkema}, annote = {Publik Printout available}, abstract = {The continuous increase of system complexity — stimulated by the higher complexity of the functionality provided by software-based embedded controllers and by the huge improvement in the computational power of hardware — requires a corresponding increase in the capability of design and safety engineers to maintain adequate safety and reliability levels. Emerging techniques, like formal methods, have the potential of dealing with the growing complexity of such systems and are increasingly being used for the development of critical systems (e.g. aircraft systems, nuclear plants, railways systems), where at stake are not only delays in delivering products and economical losses, but also environmental hazards and public confidence. However, the use of formal meth- ods during certain critical system development phases, e.g. safety analysis, is still at an early stage. In this paper we propose a new methodology, based on these novel techniques and supported by commercial and state-of-the-art tools, whose goal is to improve the safety analysis practices carried out during the development and certification of complex systems. The key ingredient of our methodology is the use of formal methods during both system development and safety analysis. This allows for a tighter integration of safety assessment and system development activities, fast system prototyping, automated safety assessment since the early stages of development, and tool- supported verification and validation.}, pub_type = {conference}, location = {Maastricht, The Netherlands}, category = {safety_analysis} }

  51. Bozzano, M., & Villafiorita, A. (2003). Integrating Fault Tree Analysis with Event Ordering Information. In Proceedings of the European Safety and Reliability Conference 2003 (ESREL 2003). Balkema. [Abstract] Fault tree analysis is a traditional and well-established technique for analyzing system design and robustness. Its purpose is to identify sets of basic events, called cut sets, which can cause a given top level event, e.g., a system malfunction, to occur. In this paper we present an algorithm that extracts ordering infor- mation, i.e., finds out possible ordering constraints which are required to hold between basic events in a cut set. The algorithm is completely automatic, and has been incorporated into a more general framework, based on model checking techniques, for automatic fault tree generation and analysis. @inproceedings{Bozzano:2003ts, author = {Bozzano, Marco and Villafiorita, Adolfo}, title = {Integrating Fault Tree Analysis with Event Ordering Information}, booktitle = {Proceedings of the European Safety and Reliability Conference 2003 (ESREL 2003)}, year = {2003}, publisher = {Balkema}, annote = {Publik Printout available}, abstract = {Fault tree analysis is a traditional and well-established technique for analyzing system design and robustness. Its purpose is to identify sets of basic events, called cut sets, which can cause a given top level event, e.g., a system malfunction, to occur. In this paper we present an algorithm that extracts ordering infor- mation, i.e., finds out possible ordering constraints which are required to hold between basic events in a cut set. The algorithm is completely automatic, and has been incorporated into a more general framework, based on model checking techniques, for automatic fault tree generation and analysis.}, pub_type = {conference}, location = {Maastricht, The Netherlands}, category = {safety_analysis} }

  52. Villafiorita, A. (1998). Abstraction as a Form of Elaboration Tolerance. In Proceedings of 8th International Conference on Artificial Intelligence: Methodology, Systems, and Applications (AIMSA98) (pp. 427–437). Springer. [Abstract] Elaboration tolerance is «the ability of accepting changes to a person’s or a computer program’s representation of facts without starting all over» [8]. In this paper we investigate how abstraction (in the sense of [5]) helps in achieving a certain degree of elaboration tolerance. We do so by mechanizing in absfol (an interactive theorem prover with abstraction) two famous representations of the missionaries and cannibals problem and by showing how abstraction helps in finding solutions in such representations «\ldots without starting all over.» @inproceedings{Villafiorita:1998pb, author = {Villafiorita, Adolfo}, title = {Abstraction as a Form of Elaboration Tolerance}, booktitle = {Proceedings of 8th International Conference on Artificial Intelligence: Methodology, Systems, and Applications (AIMSA98)}, year = {1998}, pages = {427–437}, publisher = {Springer}, annote = {Publik Printout available}, abstract = {Elaboration tolerance is «the ability of accepting changes to a person’s or a computer program’s representation of facts without starting all over» [8]. In this paper we investigate how abstraction (in the sense of [5]) helps in achieving a certain degree of elaboration tolerance. We do so by mechanizing in absfol (an interactive theorem prover with abstraction) two famous representations of the missionaries and cannibals problem and by showing how abstraction helps in finding solutions in such representations «\ldots without starting all over.»}, pub_type = {conference}, location = {Sozopol, Bulgaria}, category = {theorem_proving} }

  53. Cimatti, A., Pieraccini, P. L., Sebastiani, R., Traverso, P., & Villafiorita, A. (1999). Formal Specification and validation of a Vital Communication Protocol. In Proceedings of FM99, World Congress on Formal methods in the Development of Computing Systems (pp. 1584–1604). Springer. @inproceedings{Cimatti:1999xr, author = {Cimatti, Alessandro and Pieraccini, Pier Luigi and Sebastiani, Roberto and Traverso, Paolo and Villafiorita, Adolfo}, title = {Formal Specification and validation of a Vital Communication Protocol}, booktitle = {Proceedings of FM99, World Congress on Formal methods in the Development of Computing Systems}, year = {1999}, pages = {1584–1604}, month = sep, publisher = {Springer}, annote = {Publik Printout available}, pub_type = {conference}, location = {Toulouse, France}, category = {formal_methods}, month_numeric = {9} }

  54. Tiella, R., Villafiorita, A., & Tomasi, S. (2007). FSMC+, a tool for the generation of Java code from statecharts. In Proceedings of the 5th international symposium on Principles and practice of programming in Java (PPPJ-07) (pp. 93–102). ACM. [Abstract] ProVotE is a two-phase project aiming at actuating art. 84 of law 2 - 5/3/2003 of the Autonomous Province of Trento (Italy), which promotes the introduction of e-voting systems for the next provincial elections in Trentino (Nov. 2008). During the first phase of the ProVotE project we built jprovote, a Java/Linux e-voting system. The jprovote system has been used with experimental value by more than 11000 voters during local elections held in various municipalities of Trentino (Italy). A critical component of jprovote is its core logic, that is responsible of controlling the overall behavior of the e-voting machine during an election. In order to simplify its development and to allow for formal verification of this critical component we developed FSMC+. FSMC+ is a compiler that takes as input a subset of UML Statecharts and produces the corresponding Java and NuSMV code (NuSMV is a model checker developed at ITC-irst). Support for parameters in events, complex expressions in guards, and support to nested states are some of the distinguishing features of FSMC+. In this paper we present FSMC+ and we show how we used it for the development and the verification of the ProVotE e-voting machine. Even though FSMC+ has been specifically created to ease the development of jProvote, we believe the approach and the tool we developed to be general enough to be used in other applications. @inproceedings{Tiella:2007kb, author = {Tiella, Roberto and Villafiorita, Adolfo and Tomasi, Silvia}, title = {FSMC+, a tool for the generation of Java code from statecharts}, booktitle = {Proceedings of the 5th international symposium on Principles and practice of programming in Java (PPPJ-07)}, year = {2007}, pages = {93–102}, month = sep, publisher = {ACM}, annote = {Publik Printout available}, abstract = {ProVotE is a two-phase project aiming at actuating art. 84 of law 2 - 5/3/2003 of the Autonomous Province of Trento (Italy), which promotes the introduction of e-voting systems for the next provincial elections in Trentino (Nov. 2008). During the first phase of the ProVotE project we built jprovote, a Java/Linux e-voting system. The jprovote system has been used with experimental value by more than 11000 voters during local elections held in various municipalities of Trentino (Italy). A critical component of jprovote is its core logic, that is responsible of controlling the overall behavior of the e-voting machine during an election. In order to simplify its development and to allow for formal verification of this critical component we developed FSMC+. FSMC+ is a compiler that takes as input a subset of UML Statecharts and produces the corresponding Java and NuSMV code (NuSMV is a model checker developed at ITC-irst). Support for parameters in events, complex expressions in guards, and support to nested states are some of the distinguishing features of FSMC+. In this paper we present FSMC+ and we show how we used it for the development and the verification of the ProVotE e-voting machine. Even though FSMC+ has been specifically created to ease the development of jProvote, we believe the approach and the tool we developed to be general enough to be used in other applications.}, pub_type = {conference}, location = {Lisboa, Portugal}, category = {evoting}, month_numeric = {9} }

scientific_dissemination

  1. Villafiorita, A. (2018). Agricoltura e Informatica, un binomio vincente. Agricoltura Trentina, XXXVII(2), 8–9. @article{villafiorita18:_agric_infor, author = {Villafiorita, Adolfo}, title = {Agricoltura e Informatica, un binomio vincente}, journal = {Agricoltura Trentina}, year = {2018}, volume = {XXXVII}, number = {2}, pages = {8-9}, month = feb, pub_type = {scientific_dissemination}, category = {food}, month_numeric = {2} }

  2. Ciaghi, A., & Villafiorita, A. (2015). Combattere lo spreco e la povertà alimentare con la tecnologia. Economia Trentina, (4), 58–62. @article{ciaghi15:_combat, author = {Ciaghi, Aaron and Villafiorita, Adolfo}, title = {Combattere lo spreco e la povertà alimentare con la tecnologia}, journal = {Economia Trentina}, year = {2015}, number = {4}, pages = {58-62}, note = {In Italian}, pub_type = {scientific_dissemination}, category = {food} }

  3. Villafiorita, A. (2015). Tecnologie per combattere lo spreco alimentare. Scienze e Ricerche, Supplemento 2(7), 72–75. [Download] [Abstract] Secondo alcune stime, solo in Italia ogni anno si sprecano circa 6 milioni di tonnellate di alimenti, per un valore economico di circa 13 miliardi di euro. Allo stesso tempo molte famiglie vivono sulla soglia della povertà e faticano a trovare le risorse per andare avanti. Le nuove tecnologie possono e dovrebbero fare qualcosa per mitigare questa situazione. Questo articolo presenta la nostra esperienza con BringTheFood, una applicazione per lo scambio di cibo. @article{villafiorita15:_tecnol, author = {Villafiorita, Adolfo}, title = {Tecnologie per combattere lo spreco alimentare}, journal = {Scienze e Ricerche}, year = {2015}, volume = {Supplemento 2}, number = {7}, pages = {72-75}, month = may, note = {In Italian}, link = {http://www.scienze-ricerche.it/wp-content/uploads/2015/05/Questioni-di-cibo-maggio-20152.pdf}, abstract = {Secondo alcune stime, solo in Italia ogni anno si sprecano circa 6 milioni di tonnellate di alimenti, per un valore economico di circa 13 miliardi di euro. Allo stesso tempo molte famiglie vivono sulla soglia della povertà e faticano a trovare le risorse per andare avanti. Le nuove tecnologie possono e dovrebbero fare qualcosa per mitigare questa situazione. Questo articolo presenta la nostra esperienza con BringTheFood, una applicazione per lo scambio di cibo.}, pub_type = {scientific_dissemination}, category = {food}, month_numeric = {5} }

workshop

  1. Grau, I., Travassos, G., Cernuzzi, L., & Villafiorita, A. (2014). Tape Mbo’e: A First Experimental Assessment. In 11th Experimental Software Engineering Track Workshop (ESELAW), XVII Ibero-American Conference on Software Engineering (CIbSE). [Abstract] The development of software needs not only to consider the construction process, but also other aspects such as cost, human resources and communication among stakeholders. The lack of simplicity into this context becomes explicit when some restrictions such as service oriented must be considered as the basic architecture style to build sustainable applications into environments were practitioners are not aware of this software technology. Besides this, most of the available software processes are not direct applicable neither reusable making the learning time risky to the development of the project. Therefore, Tape Mbo’e (TME) had been proposed to strive the building of such applications, into development environments like developing country where we can have economic constraints and scarcity of proficient practitioners. TME is being used to develop a software application whose goal is to provide the interoperability among legacy systems of distinct public agencies in Paraguay. To observe TME’s use, observational studies have been executed to reveal TME’s feasibility and applicability in supporting public agencies to organize their software projects. Initial results indicated the feasibility and simplicity of TME when applied in the field. Therefore, an experience accomplished into a Paraguayan public agency is presented in this paper. @inproceedings{GR-14, author = {Grau, I. and Travassos, G. and Cernuzzi, L. and Villafiorita, A.}, title = {Tape Mbo’e: A First Experimental Assessment}, booktitle = {11th Experimental Software Engineering Track Workshop (ESELAW), XVII Ibero-American Conference on Software Engineering (CIbSE)}, year = {2014}, month = apr, abstract = {The development of software needs not only to consider the construction process, but also other aspects such as cost, human resources and communication among stakeholders. The lack of simplicity into this context becomes explicit when some restrictions such as service oriented must be considered as the basic architecture style to build sustainable applications into environments were practitioners are not aware of this software technology. Besides this, most of the available software processes are not direct applicable neither reusable making the learning time risky to the development of the project. Therefore, Tape Mbo’e (TME) had been proposed to strive the building of such applications, into development environments like developing country where we can have economic constraints and scarcity of proficient practitioners. TME is being used to develop a software application whose goal is to provide the interoperability among legacy systems of distinct public agencies in Paraguay. To observe TME’s use, observational studies have been executed to reveal TME’s feasibility and applicability in supporting public agencies to organize their software projects. Initial results indicated the feasibility and simplicity of TME when applied in the field. Therefore, an experience accomplished into a Paraguayan public agency is presented in this paper.}, pub_type = {workshop}, owner = {Ilse}, timestamp = {2014.10.21}, category = {egov4dev_countries}, month_numeric = {4} }

  2. Weldemariam, K., Mattioli, A., & Villafiorita, A. (2009). Managing Requirements for E-Voting Systems: Issues and Approaches Motivated by a Case Study. In Requirements Engineering for e-Voting Systems (RE-VOTE), 2009 First International Workshop on (pp. 29–37). https://doi.org/10.1109/RE-VOTE.2009.7 [Link] [Abstract] This paper discusses our approach and experiences on structuring and maintaining requirements for an e- voting system we have built and deployed for elections. Issues related to integrating laws and recommendation for e-voting systems, managing different elections and configurations, supporting a spiral development, yielded problems and approaches to help maintain integrity of requirements and a coherent view of the system. Moreover, the relationship between requirements and system architecture is based on finite state machines, that bridge the gap between the laws and the actual behavior of the machine. @inproceedings{5460389, author = {Weldemariam, Komminist and Mattioli, Andrea and Villafiorita, Adolfo}, title = {Managing Requirements for E-Voting Systems: Issues and Approaches Motivated by a Case Study}, booktitle = {Requirements Engineering for e-Voting Systems (RE-VOTE), 2009 First International Workshop on}, year = {2009}, pages = {29 -37}, month = aug, abstract = {This paper discusses our approach and experiences on structuring and maintaining requirements for an e- voting system we have built and deployed for elections. Issues related to integrating laws and recommendation for e-voting systems, managing different elections and configurations, supporting a spiral development, yielded problems and approaches to help maintain integrity of requirements and a coherent view of the system. Moreover, the relationship between requirements and system architecture is based on finite state machines, that bridge the gap between the laws and the actual behavior of the machine.}, doi = {10.1109/RE-VOTE.2009.7}, pub_type = {workshop}, category = {evoting}, link = {http://dx.doi.org/10.1109/RE-VOTE.2009.7}, month_numeric = {8} }

  3. Al-Shammari, A. F. N., Weldemariam, K., Villafiorita, A., & Tessaris, S. (2011). Vote verification through open standard: A roadmap. In Requirements Engineering for Electronic Voting Systems (REVOTE), 2011 International Workshop on (pp. 22–26). https://doi.org/10.1109/REVOTE.2011.6045912 [Link] [Abstract] As the technology for e-voting changes day by day along with an evolution of the regulatory environment, many questions emerge. One of these questions is how to allow voters or any third party to verify votes are correctly captured, stored and counted. This underlines the fact that an e-voting system is not only responsible for ensuring its technical and procedural security, but also must provide a mechanism by which voters can verify their votes during and after casting, and third party be able to verify the correctness and integrity of election results. The purpose of this paper is to review currently deployed vote verification methods, by discuss their weaknesses with the aim of proposing a more reliable and robust vote verification method. @inproceedings{6045912, author = {Al-Shammari, Ali Fawzi Najm and Weldemariam, Komminist and Villafiorita, Adolfo and Tessaris, Sergio}, title = {Vote verification through open standard: A roadmap}, booktitle = {Requirements Engineering for Electronic Voting Systems (REVOTE), 2011 International Workshop on}, year = {2011}, pages = {22 -26}, month = aug, abstract = {As the technology for e-voting changes day by day along with an evolution of the regulatory environment, many questions emerge. One of these questions is how to allow voters or any third party to verify votes are correctly captured, stored and counted. This underlines the fact that an e-voting system is not only responsible for ensuring its technical and procedural security, but also must provide a mechanism by which voters can verify their votes during and after casting, and third party be able to verify the correctness and integrity of election results. The purpose of this paper is to review currently deployed vote verification methods, by discuss their weaknesses with the aim of proposing a more reliable and robust vote verification method.}, doi = {10.1109/REVOTE.2011.6045912}, pub_type = {workshop}, category = {evoting}, link = {http://dx.doi.org/10.1109/REVOTE.2011.6045912}, month_numeric = {8} }

  4. Eshete, B., Villafiorita, A., & Weldemariam, K. (2011). Malicious Website Detection: Effectiveness and Efficiency Issues. In Proceedings of SysSec 2011. Amsterdam. [Link] [Abstract] Malicious websites, when visited by an unsuspecting victim infect her machine to steal invaluable information, redirect her to malicious targets or compromise her system to mount future attacks. While the existing approaches have promising prospects in detecting malicious websites, there are still open issues in effectively and efficiently addressing: filtering of web pages from the wild, coverage of wide range of malicious characteristics to capture the big picture, continuous evolution of web page features, systematic combination of fea- tures, semantic implications of feature values on characterizing web pages, ease and cost of flexibility and scalability of analysis and detection techniques with respect to inevitable changes to the threat landscape. In this position paper, we highlight our ongoing efforts towards effective and efficient analysis and detection of malicious websites with a particular emphasis on broader feature space and attack-payloads, flexibility of techniques with changes in malicious characteristics and web pages and above all real-life usability of techniques in defending users against malicious websites. @inproceedings{Eshete:2011fk, author = {Eshete, Birhanu and Villafiorita, Adolfo and Weldemariam, Komminist}, title = {Malicious Website Detection: Effectiveness and Efficiency Issues}, booktitle = {Proceedings of SysSec 2011}, year = {2011}, month = jul, address = {Amsterdam}, abstract = {Malicious websites, when visited by an unsuspecting victim infect her machine to steal invaluable information, redirect her to malicious targets or compromise her system to mount future attacks. While the existing approaches have promising prospects in detecting malicious websites, there are still open issues in effectively and efficiently addressing: filtering of web pages from the wild, coverage of wide range of malicious characteristics to capture the big picture, continuous evolution of web page features, systematic combination of fea- tures, semantic implications of feature values on characterizing web pages, ease and cost of flexibility and scalability of analysis and detection techniques with respect to inevitable changes to the threat landscape. In this position paper, we highlight our ongoing efforts towards effective and efficient analysis and detection of malicious websites with a particular emphasis on broader feature space and attack-payloads, flexibility of techniques with changes in malicious characteristics and web pages and above all real-life usability of techniques in defending users against malicious websites.}, pub_type = {workshop}, category = {web_development}, link = {http://www.syssec-project.eu/events/1st-syssec-workshop-program/}, month_numeric = {7} }

  5. Ciaghi, A., & Villafiorita, A. (2010). Towards a Law Modeling Framework to Support Law-Making via {BPR}. In Proceedings of the First Workshop on Law Compliancy Issues in Organisational Systems and Strategies. [Abstract] This paper presents a law modeling framework called VLPM 2.0 that aims at providing support to the application of BPR on Public Administration procedures. The tool leverages the existing technologies for legal documents markup and for process modeling and relies o<n semantic technologies to bind process model elements to elements in the texts. In this paper we discuss the motivations and the possible roles of such framework in the lifecycle of laws. @inproceedings{Ciaghi:2010fk, author = {Ciaghi, Aaron and Villafiorita, Adolfo}, title = {Towards a Law Modeling Framework to Support Law-Making via {BPR}}, booktitle = {Proceedings of the First Workshop on Law Compliancy Issues in Organisational Systems and Strategies}, year = {2010}, abstract = {This paper presents a law modeling framework called VLPM 2.0 that aims at providing support to the application of BPR on Public Administration procedures. The tool leverages the existing technologies for legal documents markup and for process modeling and relies o<n semantic technologies to bind process model elements to elements in the texts. In this paper we discuss the motivations and the possible roles of such framework in the lifecycle of laws.}, pub_type = {workshop}, category = {ict4laws} }

  6. Cimatti, A., Pieraccini, P. L., Sebastiani, R., Traverso, P., & Villafiorita, A. (1999). Formal Specification and validation of a Vital Communication Protocol. In Proceedings of 4th International ERCIM Workshop on Formal Methods for Industrial Critical Systems. @inproceedings{Cimatti:1999xz, author = {Cimatti, Alessandro and Pieraccini, Pier Luigi and Sebastiani, Roberto and Traverso, Paolo and Villafiorita, Adolfo}, title = {Formal Specification and validation of a Vital Communication Protocol}, booktitle = {Proceedings of 4th International ERCIM Workshop on Formal Methods for Industrial Critical Systems}, year = {1999}, annote = { Printout available}, pub_type = {workshop}, category = {formal_methods} }

  7. Roveri, M., & Villafiorita, A. (1996). Using Abstraction to Prove Theorems in Boolean Algebra. In Proceedings of AISB96 Workshop on Automated Reasoning, Bridging the Gap between Theory and Practice (pp. 40–41). [Abstract] We use abstraction as a tool to simplify proofs in Boolean Algebra (BA). We mechanize proofs by abstraction in- side ABSFOL. We use OTTER to assess the effectiveness of our approach. @inproceedings{Roveri:1996fi, author = {Roveri, Marco and Villafiorita, Adolfo}, title = {Using Abstraction to Prove Theorems in Boolean Algebra}, booktitle = {Proceedings of AISB96 Workshop on Automated Reasoning, Bridging the Gap between Theory and Practice}, year = {1996}, pages = {40-41}, month = apr, annote = {Printout available}, abstract = {We use abstraction as a tool to simplify proofs in Boolean Algebra (BA). We mechanize proofs by abstraction in- side ABSFOL. We use OTTER to assess the effectiveness of our approach.}, pub_type = {workshop}, location = {Brighton, UK}, category = {theorem_proving}, month_numeric = {4} }

  8. Villafiorita, A., & Giunchiglia, F. (1996). Inductive Theorem Proving via Abstraction. In Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics (AI-MATH96). [Abstract] We use abstraction as a tool to plan proofs by induction inside ABSFOL, an interactive theorem prover with abstraction @inproceedings{Villafiorita:1996xw, author = {Villafiorita, Adolfo and Giunchiglia, Fausto}, title = {Inductive Theorem Proving via Abstraction}, booktitle = {Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics (AI-MATH96)}, year = {1996}, month = jan, annote = {Publik Printout available}, abstract = {We use abstraction as a tool to plan proofs by induction inside ABSFOL, an interactive theorem prover with abstraction}, pub_type = {workshop}, location = {Fort Lauderdale, Florida}, category = {theorem_proving}, month_numeric = {1} }

  9. Tiella, R., Villafiorita, A., & Tomasi, S. (2006). Specification of the Control Logic of an eVoting System in UML: the ProVotE experience. In Proceedings of 5th International Workshop on Critical Systems Development Using Modeling Languages (CSDUML06). [Abstract] The ProVotE project aims at actuating art. 84 of law 2 - 5/3/2003 of the Autonomous Province of Trento (Italy), which promotes the introduction of e-voting systems for the next provincial elections. The goals of the project are building an e-voting system and defining the related process and certification issues in order to deliver a solution which is compliant with the italian electoral law, that is trusted and usable by the voters, and that implements the security and dependability requirements of the best international practices and experiences. This paper presents some of the issues and challenges we faced during the development of the e-voting prototype which was tested by about 8500 voters in three different trials held during the elections for the local representatives. In particular we show how we integrated UML in the development process of the e-voting machine. We also highlight how we extended existing tools to support the formal verification of the UML specifications and how we automated the generation of a critical component of the e-voting machine using UML statecharts. @inproceedings{Tiella:2006ec, author = {Tiella, Roberto and Villafiorita, Adolfo and Tomasi, Silvia}, title = {Specification of the Control Logic of an eVoting System in UML: the ProVotE experience}, booktitle = {Proceedings of 5th International Workshop on Critical Systems Development Using Modeling Languages (CSDUML06)}, year = {2006}, month = oct, annote = {Publik Printout available}, abstract = {The ProVotE project aims at actuating art. 84 of law 2 - 5/3/2003 of the Autonomous Province of Trento (Italy), which promotes the introduction of e-voting systems for the next provincial elections. The goals of the project are building an e-voting system and defining the related process and certification issues in order to deliver a solution which is compliant with the italian electoral law, that is trusted and usable by the voters, and that implements the security and dependability requirements of the best international practices and experiences. This paper presents some of the issues and challenges we faced during the development of the e-voting prototype which was tested by about 8500 voters in three different trials held during the elections for the local representatives. In particular we show how we integrated UML in the development process of the e-voting machine. We also highlight how we extended existing tools to support the formal verification of the UML specifications and how we automated the generation of a critical component of the e-voting machine using UML statecharts.}, pub_type = {workshop}, location = {Genova, Italy}, category = {evoting}, month_numeric = {10} }

  10. Sebastiani, R., Villafiorita, A., & Giunchiglia, F. (1994). Proving Theorems by Using Abstraction Interactively. In Proceedings of the Second International Round-Table on Abstract Intelligent Agent: Situation Assessment (AIA 94). [Abstract] In this paper we show how an interactive use of abstraction in theorem proving can improve the comprehension and reduce the complexity of many significant problems. For such a task we present a fully mechanized example of the very well-know map colouring problem. @inproceedings{Sebastiani:1994xd, author = {Sebastiani, Roberto and Villafiorita, Adolfo and Giunchiglia, Fausto}, title = {Proving Theorems by Using Abstraction Interactively}, booktitle = {Proceedings of the Second International Round-Table on Abstract Intelligent Agent: Situation Assessment (AIA 94)}, year = {1994}, annote = {Publik Two printouts available (AIA + Scriftenreihe)}, abstract = {In this paper we show how an interactive use of abstraction in theorem proving can improve the comprehension and reduce the complexity of many significant problems. For such a task we present a fully mechanized example of the very well-know map colouring problem.}, pub_type = {workshop}, category = {theorem_proving} }

  11. Villafiorita, A., & Sebastiani, R. (1994). Proof planning by abstraction. In Proceedings of ECAI94 Workshop From Theorem Provers to Mathematical Assistants (pp. 15–24). [Abstract] Devising powerful heuristics or shifting the control to humans have probably been the two most common solutions to keep the search space in theorem proving manageable. In this paper we take advantage of both, by using abstraction as a tool to plan proofs by induction and by proving its effectiveness in ABSFOL (an interactive theorem prover built on top of GETFOL) @inproceedings{Villafiorita:1994fy, author = {Villafiorita, Adolfo and Sebastiani, Roberto}, title = {Proof planning by abstraction}, booktitle = {Proceedings of ECAI94 Workshop From Theorem Provers to Mathematical Assistants}, year = {1994}, pages = {15–24}, month = aug, annote = {Publik Printout available}, abstract = {Devising powerful heuristics or shifting the control to humans have probably been the two most common solutions to keep the search space in theorem proving manageable. In this paper we take advantage of both, by using abstraction as a tool to plan proofs by induction and by proving its effectiveness in ABSFOL (an interactive theorem prover built on top of GETFOL)}, pub_type = {workshop}, location = {Amsterdam, The Netherlands}, category = {theorem_proving}, month_numeric = {8} }

  12. Cimatti, A., Giunchiglia, F., Traverso, P., & Villafiorita, A. (1999). Run-Time Result Formal Verification of Safety Critical Software: an Industrial Case Study. In Proceedings of FLoC99 Workshop on Run-Time Result Verification. [Abstract] In this paper we describe an industrial project whose goal was the certification of the translator part of a tool used to develop safety critical applications. We have successfully applied a novel formal verification technique. We have constructed an Embedded Verifier which, for each run of the translator, verifies formally the correctness of the result of each translation, rather than the correctness of the translation algorithm or code. We call this approach Run-time Result Formal Verification. In order to satisfy efficiency requirements on the Embedded Verifier, we have decomposed the proof of correctness into two parts. The task of the Embedded Verifier is to prove some simple conditions at each run (on-line proof), that have been proved once for all to guarantee the correctness of the translation (off-line proof). We have addressed the problem of the correctness of the implementation of the Embedded Verifier itself by decomposing it into two independent programs, such that only a small kernel of the verifier is critical. @inproceedings{Cimatti:1999rw, author = {Cimatti, Alessandro and Giunchiglia, Fausto and Traverso, Paolo and Villafiorita, Adolfo}, title = {Run-Time Result Formal Verification of Safety Critical Software: an Industrial Case Study}, booktitle = {Proceedings of FLoC99 Workshop on Run-Time Result Verification}, year = {1999}, annote = {Publik Printout NOT available}, abstract = {In this paper we describe an industrial project whose goal was the certification of the translator part of a tool used to develop safety critical applications. We have successfully applied a novel formal verification technique. We have constructed an Embedded Verifier which, for each run of the translator, verifies formally the correctness of the result of each translation, rather than the correctness of the translation algorithm or code. We call this approach Run-time Result Formal Verification. In order to satisfy efficiency requirements on the Embedded Verifier, we have decomposed the proof of correctness into two parts. The task of the Embedded Verifier is to prove some simple conditions at each run (on-line proof), that have been proved once for all to guarantee the correctness of the translation (off-line proof). We have addressed the problem of the correctness of the implementation of the Embedded Verifier itself by decomposing it into two independent programs, such that only a small kernel of the verifier is critical. }, pub_type = {workshop}, location = {Trento, Italy}, category = {formal_methods} }

  13. Villafiorita, A. (1995). Reasoning by Analogy via Abstraction. In Proceedings of the Symposium on Abstraction, Reformulation and Approximation, SARA-95 (pp. 156–162). [Abstract] Abstraction has been used in theorem proving as a heuristic to reduce the search space (see, for instance, [Simpson, 1988]) and as a tool for explanation (see, for instance, [Bundy et al., 1993]). We use abstraction to model certain forms of reasoning by analogy. @inproceedings{Villafiorita:1995la, author = {Villafiorita, Adolfo}, title = {Reasoning by Analogy via Abstraction}, booktitle = {Proceedings of the Symposium on Abstraction, Reformulation and Approximation, SARA-95}, year = {1995}, pages = {156–162}, month = aug, annote = {Publik Printout available}, abstract = {Abstraction has been used in theorem proving as a heuristic to reduce the search space (see, for instance, [Simpson, 1988]) and as a tool for explanation (see, for instance, [Bundy et al., 1993]). We use abstraction to model certain forms of reasoning by analogy.}, pub_type = {workshop}, location = {Ville d’Esterel, Canada}, category = {theorem_proving}, month_numeric = {8} }