function format_seconds()
{
    awk '{
    hr=($1/3600); hd=(sprintf("%02d", hr))
    mr=((hr-hd)*60); md=(sprintf("%02d", mr))
    s=((mr-md)*60); sd=(sprintf("%02d", s))
    t=(sprintf("%02d:%02d:%06.3f" ,hd,md,s)); print t}' <<< $1
}