Recent Publications

Matos M, Mercier H, Felber P, Oliveira R, Pereira JO.  2015.  EpTO: An Epidemic Total Order Algorithm for Large-Scale Distributed Systems. Proceedings of the 16th Annual Middleware Conference. :100–111. Abstractp100-matos.pdf

n/a

Harrison M, Campos J, Masci P, Curzon P.  2015.  Templates as heuristics for proving properties of medical devices. 5th EAI International Conference on Wireless Mobile Communication and Healthcare - "Transforming healthcare through innovations in mobile and wireless technologies". antennatemplatesv5-final.pdf
Campos JC, Silva JL, Harrison M.  2015.  Supporting the Design of an Ambient Assisted Living System Using Virtual Reality Prototypes. Ambient Assisted Living. ICT-based Solutions in Real Life Situations. 9455:49-61.authorsversion.pdf
Couto M, Cunha J, Fernandes JP, Pereira R, Saraiva JA.  2015.  GreenDroid: A tool for analysing power consumption in the android ecosystem. Scientific Conference on Informatics, 2015 IEEE 13th International. :73-78. Abstractinformatics2015_51_marcocouto.pdf

n/a

Daniels W, Proença J, Matthys N, Joosen W, Hughes D.  2015.  Tomography: lowering management overhead for distributed component-based applications. Proceedings of the 2nd Workshop on Middleware for Context-Aware Applications in the IoT, M4IoT@Middleware 2015, Vancouver, BC, Canada, December 7-11, 2015. :13–18. Abstracttomography.pdf

n/a

Proença J, Clarke D.  2015.  Typed Connector Families. Formal Aspects of Component Software - 12th International Conference, FACS 2015, Niterói, Brazil, October 14-16, 2015, Revised Selected Papers. 9539:294–311. Abstractcfam.pdf

n/a

Fischer S, Hu Z, Pacheco H.  2015.  A clear picture of lens laws. Proceedings of the 12th International Conference on Mathematics of Program Construction (MPC 2015). Abstract
n/a
Costa CM, Leite CRM, Sousa AL.  2015.  Service Response Time Measurement Model of Service Level Agreements in Cloud Environment. 2015 {IEEE} International Conference on Smart City/SocialCom/SustainCom, SmartCity 2015, Chengdu, China, December 19-21, 2015. :969–974. Abstract
n/a
Silva JMC, Carvalho P, Lima SR.  2015.  Analysing traffic flows through sampling: A comparative study. 2015 IEEE Symposium on Computers and Communication (ISCC). :341-346. Abstract

n/a

Silva JMC, Carvalho P, Lima SR.  2015.  A modular sampling framework for flexible traffic analysis. 2015 23rd International Conference on Software, Telecommunications and Computer Networks (SoftCOM). :200-204. Abstract
n/a
Couto M, Cunha J, Fernandes JP, Pereira R, Saraiva J.  2015.  GreenDroid: A tool for analysing power consumption in the android ecosystem. Scientific Conference on Informatics, 2015 IEEE 13th International. :73–78. Abstract
n/a
Pontes R, Matos M, Oliveira JN, Pereira JO.  2015.  Implementing a Linear Algebra Approach to Data Processing. Grand Timely Topics in Software Engineering - International Summer School {GTTSE} 2015, Braga, Portugal, August 23-29, 2015, Tutorial Lectures. 10223:215–222. Abstract
n/a
Almeida PS, Moreno CB, Gonçalves R, Preguiça N, Fonte V.  2014.  Scalable and Accurate Causality Tracking for Eventually Consistent Stores. Distributed Applications and Interoperable Systems. 8460 Abstractdvvset-dais.pdf

In cloud computing environments, data storage systems often rely on optimistic replication to provide good performance and availability even in the presence of failures or network partitions. In this scenario, it is important to be able to accurately and efficiently identify updates executed concurrently. Current approaches to causality tracking in optimistic replication have problems with concurrent updates: they either (1) do not scale, as they require replicas to maintain information that grows linearly with the number of writes or unique clients; (2) lose information about causality, either by removing entries from client-id based version vectors or using server-id based version vectors, which cause false conflicts. We propose a new logical clock mechanism and a logical clock framework that together support a traditional key-value store API, while capturing causality in an accurate and scalable way, avoiding false conflicts. It maintains concise information per data replica, only linear on the number of replica servers, and allows data replicas to be compared and merged linear with the number of replica servers and versions.

Sousa M, Campos JC, Alves M, Harrison M.  2014.  Formal Verification of Safety-Critical User Interfaces: a space system case study. Formal Verification and Modeling in Human Machine Systems: Papers from the AAAI Spring Symposium. :62-67. Abstract7722-34384-1-pb.pdf

Safe operation of safety critical systems depends on appropriate interactions between the human operator and the computer system. Specification of such safety-critical systems is fundamental to enable exhaustive and automated analysis of operator system interaction. In this paper we present a structured, comprehensive and computer-aided approach to formally specify and verify user interfaces based on model checking techniques.

Pedro AM, Pereira D, Pinho LM, Pinto JS.  2014.  Towards a Runtime Verification Framework for the Ada Programming Language. Proceedings of the 19th International Conference on Reliable Software Technologies. Abstract2014_rstae_14.pdf

Runtime verification is an emerging discipline that investi- gates methods and tools to enable the verification of program properties during the execution of the application. The goal is to complement static analysis approaches, in particular when static verification leads to the ex- plosion of states. Non-functional properties, such as the ones present in real-time systems are an ideal target for this kind of verification method- ology, as are usually out of the range of the power and expressiveness of classic static analyses. In this paper, we present a framework that allows real-time programs written in Ada to be augmented with runtime ver- ification capabilities. Our framework provides the infrastructures which is needed to instrument the code with runtime monitors. These moni- tors are responsible for observing the system and reaching verdicts about whether its behavior is compliant with its non-functional properties. We also sketch a contract language to extend the one currently provided by Ada, with the long term goal of having an elegant way in which run- time monitors can be automatically synthesized and instrumented into the target systems. The usefulness of the proposed approach is demon- strated by showing its use for an application scenario.