Researcher profile

Petros Stefaneas

Petros Stefaneas contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
7works
0followers
4topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

7 published item(s)

preprint2012arXiv

A methodology for internal Web ethics

The vigorous impact of the Web in time and space arises from the fact that it motivates massive creation, editing and distribution of information by Users with little knowledge. This unprecedented continuum provides novel opportunities for innovation but also puts under jeopardy its survival as a stable construct that nurtures a complex system of connections. We examine the Web as an ethics determined space by demonstrating Hayek's theory of freedom in a three-leveled Web: technological, contextualized and economic. Our approach accounts for the co-dependence of code and values, and assumes that the Web is a self-contained system that exists in and by itself. This view of internal Web ethics directly connects the concept of freedom with issues like centralization of traffic and data control, rights on visiting log file, custom User profiles and the interplay among function, structure and morality of the Web. It is also demonstrated, in the case of Net Neutrality, that generic freedom-coercion trade-offs are incomplete in treating specific cases at work.

preprint2012arXiv

OTS/CafeOBJ2JML: An attempt to combine Design By Contract with Behavioral Specifications

Design by Constract (DBC) has influenced the development of formal specification languages that allow the mix of specification and implementation code, like Eiffel, the Java Modeling Language (JML) and Spec#. Meanwhile algebraic specification languages have been developing independently and offer full support for specification and verification of design for large and complex systems in a mathematical rigorous way. However there is no guarantee that the final implementation will comply to the specification. In this paper we proposed the use of the latter for the specification and verification of the systems design and then by presenting a translation between the two, the use of the former to ensure that the implementation respects the specification and thus enjoy the verified properties.

preprint2011arXiv

A Dynamic Algebraic Specification for Social Networks

With the help of the Internet, social networks have grown rapidly. This has increased security requirements. We present a formalization of social networks as composite behavioral objects, defined using the Observational Transition System (OTS) approach. Our definition is then translated to the OTS/CafeOBJ algebraic specification methodology. This translation allows the formal verification of safety properties for social networks via the Proof Score method. Finally, using this methodology we formally verify some security properties.

preprint2011arXiv

An Algebraic Specification of the Semantic Web

We present a formal specification of the Semantic Web, as an extension of the World Wide Web using the well known algebraic specification language CafeOBJ. Our approach allows the description of the key elements of the Semantic Web technologies, in order to give a better understanding of the system, without getting involved with their implementation details that might not yet be standardized. This specification is part of our work in progress concerning the modeling the Social Semantic Web.

preprint2011arXiv

Beyond the Boundaries of Open, Closed and Pirate Archives: Lessons from a Hybrid Approach

The creation of open archives i.e. archives where access is regulated by open licensing models (content, source, data), should be seen as part of a broader socio-economic phenomenon that finds legal expression in specific organizational and technical formats.This paper examines the origins and main characteristics of the open archives phenomenon. We investigate the extent to which different models of production of economic or social value can be expressed in different forms of licensing in the context of open archives. Through this process, we assess the extent to which the digital archive is moving towards providing access that is deeper (meaning, that offers more access rights) and wider (in the sense that most of the information given is in open content licensing) or face a gradual stratification and polarization of the content. Such stratification entails the emergence of two types of content: content to which access is extremely limited and content to which access remains completely open. This differentiation between classes of content is the result of multiple factors: from purely legislative, administrative and contractual restrictions (e.g. data protection and confidentiality restrictions) to information economics (e.g. peer production) or social (minimum universal access). We claim that with respect to the access management model, most of the current archiving processes include elements of openness. Usually, this is the result of economic necessity expressed in licensing instruments or organisational arrangements. The viability and the socio-economic importance of the digital archives also contributes to the use of open archiving practices. In such a context, although pure forms of open digital archives may remain an ideal, the reality of hybrid open digital archives is a necessity.

preprint2011arXiv

Transforming ASN.1 Specifications into CafeOBJ to assist with Property Checking

The adoption of algebraic specification/formal method techniques by the networks' research community is happening slowly but steadily. We work towards a software environment that can translate a protocol's specification, from Abstract Syntax Notation One (ASN.1 - a very popular specification language with many applications), into the powerful algebraic specification language CafeOBJ. The resulting code can be used to check, validate and falsify critical properties of systems, at the pre-coding stage of development. In this paper, we introduce some key elements of ASN.1 and CafeOBJ and sketch some first steps towards the implementation of such a tool including a case study.