Transit passenger segmentation using travel regularity mined from Smart Card transactions data

Transit passenger market segmentation enables transit operators to target different classes of transit users to provide customized information and services. The Smart Card (SC) data, from Automated Fare Collection system, facilitates the understanding of multiday travel regularity of transit passengers, and can be used to segment them into identifiable classes of similar behaviors and needs. However, the use of SC data for market segmentation has attracted very limited attention in the literature. This paper proposes a novel methodology for mining spatial and temporal travel regularity from each individual passenger’s historical SC transactions and segments them into four segments of transit users. After reconstructing the travel itineraries from historical SC transactions, the paper adopts the Density-Based Spatial Clustering of Application with Noise (DBSCAN) algorithm to mine travel regularity of each SC user. The travel regularity is then used to segment SC users by an a priori market segmentation approach. The methodology proposed in this paper assists transit operators to understand their passengers and provide them oriented information and services.

Passenger segmentation using smart card data

Transit passenger market segmentation enables transit operators to target different classes of transit users for targeted surveys and various operational and strategic planning improvements. However, the existing market segmentation studies in the literature have been generally done using passenger surveys, which have various limitations. The smart card (SC) data from an automated fare collection system facilitate the understanding of the multiday travel pattern of transit passengers and can be used to segment them into identifiable types of similar behaviors and needs. This paper proposes a comprehensive methodology for passenger segmentation solely using SC data. After reconstructing the travel itineraries from SC transactions, this paper adopts the density-based spatial clustering of application with noise (DBSCAN) algorithm to mine the travel pattern of each SC user. An a priori market segmentation approach then segments transit passengers into four identifiable types. The methodology proposed in this paper assists transit operators to understand their passengers and provides them oriented information and services.

A modified Density-Based Scanning Algorithm with Noise for spatial travel pattern analysis from Smart Card AFC data

Smart Card Automated Fare Collection (AFC) data has been extensively exploited to understand passenger behavior, passenger segment, trip purpose and improve transit planning through spatial travel pattern analysis. The literature has been evolving from simple to more sophisticated methods such as from aggregated to individual travel pattern analysis, and from stop-to-stop to flexible stop aggregation. However, the issue of high computing complexity has limited these methods in practical applications. This paper proposes a new algorithm named Weighted Stop Density Based Scanning Algorithm with Noise (WS-DBSCAN) based on the classical Density Based Scanning Algorithm with Noise (DBSCAN) algorithm to detect and update the daily changes in travel pattern. WS-DBSCAN converts the classical quadratic computation complexity DBSCAN to a problem of sub-quadratic complexity. The numerical experiment using the real AFC data in South East Queensland, Australia shows that the algorithm costs only 0.45% in computation time compared to the classical DBSCAN, but provides the same clustering results.

an improved smart card based password authentication scheme with provable security

Password authentication has been adopted as one of the most commonly used solutions in network environment to protect resources from unauthorized access. Recently, Lee–Kim–Yoo [S.W. Lee, H.S. Kim, K.Y. Yoo, Improvement of Chien et al.'s remote user authentication scheme using smart cards, Computer Standards & Interfaces 27 (2) (2005) 181–183] and Lee-Chiu [N.Y. Lee, Y.C. Chiu, Improved remote authentication scheme with smart card, Computer Standards & Interfaces 27 (2) (2005) 177–180] respectively proposed a smart card based password authentication scheme. We show that these two schemes are both subject to forgery attacks provided that the information stored in the smart card is disclosed by the adversary. We also propose an improved scheme with formal security proof.

A proposed smart-card solution for Australian health services : the problems encountered

This case study describes the experience of a state government health department in evaluating the use of smart card technology to redesign health benefits programs for the disabled in Australia. The social and political context of the system is explained in detail, and the potential benefits and risks accruing to the government, health care intermediaries and the community are examined.

Further observations on smart-card-based password-authenticated key agreement in distributed systems

This paper initiates the study of two specific security threats on smart-card-based password authentication in distributed systems. Smart-card-based password authentication is one of the most commonly used security mechanisms to determine the identity of a remote client, who must hold a valid smart card and the corresponding password to carry out a successful authentication with the server. The authentication is usually integrated with a key establishment protocol and yields smart-card-based password-authenticated key agreement. Using two recently proposed protocols as case studies, we demonstrate two new types of adversaries with smart card: 1) adversaries with pre-computed data stored in the smart card, and 2) adversaries with different data (with respect to different time slots) stored in the smart card. These threats, though realistic in distributed systems, have never been studied in the literature. In addition to point out the vulnerabilities, we propose the countermeasures to thwart the security threats and secure the protocols. © 2013 IEEE.

Wireless broadcast encryption based on smart cards

Wireless broadcasting is an efficient way to broadcast data to a large number of users. Some commercial applications of wireless broadcasting, such as satellite pay-TV, desire that only those users who have paid for the service can retrieve broadcast data. This is often achieved by broadcast encryption, which allows a station securely to broadcast data to a dynamically changing set of privileged users through open air. Most existing broadcast encryption schemes can only revoke a pre-specified number of users before system re-setup or require high computation, communication and storage overheads in receivers. In this paper, we propose a new broadcast encryption scheme based on smart cards. In our scheme, smart cards are used to prevent users from leaking secret keys. Additionally, once an illegally cloned smart card is captured, our scheme also allows tracing of the compromised smart card by which illegal smart cards are cloned, and can then revoke all cloned smart cards. The new features of our scheme include minimal computation needs of only a few modular multiplications in the smart card, and the capability to revoke up to any number of users in one revocation. Furthermore, our scheme is secure against both passive and active attacks and has better performance than other schemes.

JML- Based formal development of a Java card application for managing medical appointments

Although formal methods can dramatically increase the quality of software systems, they have not widely been adopted in software industry. Many software companies have the perception that formal methods are not cost-effective cause they are plenty of mathematical symbols that are difficult for non-experts to assimilate. The Java Modelling Language (short for JML) Section 3.3 is an academic initiative towards the development of a common formal specification language for Java programs, and the implementation of tools to check program correctness. This master thesis work shows how JML based formal methods can be used to formally develop a privacy sensitive Java application. This is a smart card application for managing medical appointments. The application is named HealthCard. We follow the software development strategy introduced by João Pestana, presented in Section 3.4. Our work influenced the development of this strategy by providing hands-on insight on challenges related to development of a privacy sensitive application in Java. Pestana’s strategy is based on a three-step evolution strategy of software specifications, from informal ones, through semiformal ones, to JML formal specifications. We further prove that this strategy can be automated by implementing a tool that generates JML formal specifications from a welldefined subset of informal software specifications. Hence, our work proves that JML-based formal methods techniques are cost-effective, and that they can be made popular in software industry. Although formal methods are not popular in many software development companies, we endeavour to integrate formal methods to general software practices. We hope our work can contribute to a better acceptance of mathematical based formalisms and tools used by software engineers. The structure of this document is as follows. In Section 2, we describe the preliminaries of this thesis work. We make an introduction to the application for managing medical applications we have implemented. We also describe the technologies used in the development of the application. This section further illustrates the Java Card Remote Method Invocation communication model used in the medical application for the client and server applications. Section 3 introduces software correctness, including the design by contract and the concept of contract in JML. Section 4 presents the design structure of the application. Section 5 shows the implementation of the HealthCard. Section 6 describes how the HealthCard is verified and validated using JML formal methods tools. Section 7 includes some metrics of the HealthCard implementation and specification. Section 8 presents a short example of how a client-side of a smart card application can be implemented while respecting formal specifications. Section 9 describes a prototype tools to generate JML formal specifications from informal specifications automatically. Section 10 describes some challenges and main ideas came acrorss during the development of the HealthCard. The full formal specification and implementation of the HealthCard smart card application presented in this document can be reached at https://sourceforge.net/projects/healthcard/.

e-Pontos: Uma solução embarcada de automação comercial aplicada a clubes de fidelidade baseado em tecnologia RFID e esmart card

In practically all vertical markets and in every region of the planet, loyalty marketers have adopted the tactic of recognition and reward to identify, maintain and increase the yield of their customers. Several strategies have been adopted by companies, and the most popular among them is the loyalty program, which displays a loyalty club to manage these rewards. But the problem with loyalty programs is that customer identification and transfer of loyalty points are made in a semiautomatic. Aiming at this, this paper presents a master's embedded business automation solution called e-Points. The goal of e-Points is munir clubs allegiances with fully automated tooling technology to identify customers directly at the point of sales, ensuring greater control over the loyalty of associate members. For this, we developed a hardware platform with embedded system and RFID technology to be used in PCs tenant, a smart card to accumulate points with every purchase and a web server, which will provide services of interest to retailers and customers membership to the club

BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B

Java Card technology allows the development and execution of small applications embedded in smart cards. A Java Card application is composed of an external card client and of an application in the card that implements the services available to the client by means of an Application Programming Interface (API). Usually, these applications manipulate and store important information, such as cash and confidential data of their owners. Thus, it is necessary to adopt rigor on developing a smart card application to improve its quality and trustworthiness. The use of formal methods on the development of these applications is a way to reach these quality requirements. The B method is one of the many formal methods for system specification. The development in B starts with the functional specification of the system, continues with the application of some optional refinements to the specification and, from the last level of refinement, it is possible to generate code for some programming language. The B formalism has a good tool support and its application to Java Card is adequate since the specification and development of APIs is one of the major applications of B. The BSmart method proposed here aims to promote the rigorous development of Java Card applications up to the generation of its code, based on the refinement of its formal specification described in the B notation. This development is supported by the BSmart tool, that is composed of some programs that automate each stage of the method; and by a library of B modules and Java Card classes that model primitive types, essential Java Card API classes and reusable data structures

KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B

The development of smart card applications requires a high level of reliability. Formal methods provide means for this reliability to be achieved. The BSmart method and tool contribute to the development of smart card applications with the support of the B method, generating Java Card code from B specifications. For the development with BSmart to be effectively rigorous without overloading the user it is important to have a library of reusable components built in B. The goal of KitSmart is to provide this support. A first research about the composition of this library was a graduation work from Universidade Federal do Rio Grande do Norte, made by Thiago Dutra in 2006. This first version of the kit resulted in a specification of Java Card primitive types byte, short and boolean in B and the creation of reusable components for application development. This work provides an improvement of KitSmart with the addition of API Java Card specification made in B and a guide for the creation of new components. The API Java Card in B, besides being available to be used for development of applications, is also useful as a documentation of each API class. The reusable components correspond to modules to manipulate specific structures, such as date and time. These structures are not available for B or Java Card. These components for Java Card are generated from specifications formally verified in B. The guide contains quick reference on how to specify some structures and how some situations were adapted from object-orientation to the B Method. This work was evaluated through a case study made through the BSmart tool, that makes use of the KitSmart library. In this case study, it is possible to see the contribution of the components in a B specification. This kit should be useful for B method users and Java Card application developers

Effects of fare collection policy on operating characteristics of a Brisbane busway station

Transit agencies across the world are increasingly shifting their fare collection mechanisms towards fully automated systems like the smart card. One of the objectives in implementing such a system is to reduce the boarding time per passenger and hence reduce the overall dwell time for the buses at the bus stops/bus rapid transit (BRT) stations. TransLink, the transit authority responsible for public transport management in South East Queensland, has introduced ‘GoCard’ technology using the Cubic platform for fare collection on its public transport system. In addition to this, three inner city BRT stations on South East Busway spine are operating as pre-paid platforms during evening peak time. This paper evaluates the effects of these multiple policy measures on operation of study busway station. The comparison between pre and post policy scenarios suggests that though boarding time per passenger has decreased, while the alighting time per passenger has increased slightly. However, there is a substantial reduction in operating efficiency was observed at the station.

AITPM Email Newsletter Volume 0911, November 2009 : President's Message

President’s Report Hello fellow AITPM members, It is interesting to follow the news at present, where transport costs are getting a significant airing. Treasury Secretary Dr Ken Henry has enunciated something Australians may have considered extremely radical just a few years back, but in the present time appears to quite a few to be a realistic alternative. That being a rethink of the way we are charged for using our vehicles. It appears that serious consideration is being given to congestion charging, perhaps in place at least to some extent, of fuel excise. As a transport professional I am pleased that the debate has elevated to the national level, and would look forward that AITPM might contribute appropriately to it. As a motorist though, I naturally have my concerns about being hit in the hip pocket. Not that I actually drive during congested periods very much. I am fortunate to live five minutes either side of two well serviced bus corridors, one of which will eventually become a busway, and work in the central business district, which is hub from all spokes in Brisbane. As such, bus and foot are my preferred commute modes. Ah but I should not gloat, as my smart card fare is about to increase by 20 percent in the New Year! And if the newspapers are to be believed, further substantial increments are proposed over the coming few years. This is reported to recoup some more of the costs of actually providing the quality public transport system that we enjoy in our region. So I expect it will be very interesting to see how transport economics will play out in reality in the coming few years, and how governments cater to Australians who either cannot afford substantial increases in transport costs or have no viable alternatives to those facilities whose costs will increase. The 2010 AITPM National Conference, “What’s New?”, still has the opportunity for authors to submit an abstract for consideration so please consider how you might contribute to the event. Best regards to all, Jon Bunker